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

case mpr
x y : Class
⊢ (∃ z, z ∈ x ∧ y ∈ z) → y ∈ ⋃₀ x
x y : Class
⊢ y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z
constructor
case mp.intro.intro.intro.intro
x : Class
w : ZFSet
z : Set ZFSet
hzx : z ∈ classToCong x
hwz : w ∈ z
⊢ ∃ z, z ∈ x ∧ ↑w ∈ z
case mp
x y : Class
⊢ y ∈ ⋃₀ x → ∃ z, z ∈ x ∧ y ∈ z
rintro ⟨w, rfl, z, hzx, hwz⟩
no goals
case mp.intro.intro.intro.intro
x : Class
w : ZFSet
z : Set ZFSet
hzx : z ∈ classToCong x
hwz : w ∈ z
⊢ ∃ z, z ∈ x ∧ ↑w ∈ z
exact ⟨z, hzx, coe_mem.2 hwz⟩
case mpr.intro.intro.intro.intro
x w : Class
hwx : w ∈ x
z : ZFSet
hwz : w z
⊢ ↑z ∈ ⋃₀ x
case mpr
x y : Class
⊢ (∃ z, z ∈ x ∧ y ∈ z) → y ∈ ⋃₀ x
rintro ⟨w, hwx, z, rfl, hwz⟩
no goals
case mpr.intro.intro.intro.intro
x w : Class
hwx : w ∈ x
z : ZFSet
hwz : w z
⊢ ↑z ∈ ⋃₀ x
exact ⟨z, rfl, w, hwx, hwz⟩