x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ⊆ x
z : ZFSet
hz : z ∈ y
⊢ z ⊆ x
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ powerset x
z : ZFSet
hz : z ∈ y
⊢ z ∈ powerset x
rw [mem_powerset] at hy⊢
no goals
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ⊆ x
z : ZFSet
hz : z ∈ y
⊢ z ⊆ x
exact h.subset_of_mem (hy hz)