Theorem: SetTheory.mem_π₂_iff (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ π₂ x ↔ ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
Tactic:
unfold π₂
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      ⋃
        sep
          (BoundedFormula.imp (BoundedFormula.ne (Sum.inl true) (Sum.inl false))
            (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inl false))))
          (fun i => if i = true then ⋃ x else ⋂ x) (⋃ x) ↔
    ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      ⋃
        sep
          (BoundedFormula.imp (BoundedFormula.ne (Sum.inl true) (Sum.inl false))
            (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inl false))))
          (fun i => if i = true then ⋃ x else ⋂ x) (⋃ x) ↔
    ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
Tactic:
aesop
State after:
no goals