Theorem: SetTheory.mem_union_iff (SetTheory/Axioms.lean)

State before:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
Tactic:
show z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y
State after:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y

State before:
V : Type u_1
inst✝³ inst✝² : SetTheory V
inst✝¹ : Union V
inst✝ : Pairing V
x y z : V
⊢ z ∈ ⋃ pair x y ↔ z ∈ x ∨ z ∈ y
Tactic:
aesop
State after:
no goals