x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∧ z ∈ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∩ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∩ y
rw [mem_inter] at hz⊢
no goals
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∧ z ∈ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩