case mp
x : Class
y : ZFSet
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

case mpr
x : Class
y : ZFSet
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
x : Class
y : ZFSet
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z
constructor
case mp.intro.intro.intro.intro
x : Class
y z : ZFSet
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z
case mp
x : Class
y : ZFSet
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z
rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
no goals
case mp.intro.intro.intro.intro
x : Class
y z : ZFSet
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z
exact ⟨z, hxz, hyz⟩
no goals
case mpr
x : Class
y : ZFSet
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩