Theorem: SetTheory.π₁_opair (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₁ (opair x y) = x
Tactic:
unfold π₁ opair
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ⋃ ⋂ pair {x} (pair x y) = x

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ⋃ ⋂ pair {x} (pair x y) = x
Tactic:
ext z
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ ⋃ ⋂ pair {x} (pair x y) ↔ z ∈ x

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ ⋃ ⋂ pair {x} (pair x y) ↔ z ∈ x
Tactic:
aesop
State after:
no goals