This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axun2

Description: A variant of the Axiom of Union ax-un . For any set x , there exists a set y whose members are exactly the members of the members of x i.e. the union of x . Axiom Union of BellMachover p. 466. (Contributed by NM, 4-Jun-2006)

Ref Expression
Assertion axun2 ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w z ∈ w ∧ w ∈ x

Proof

Step Hyp Ref Expression
1 ax-un ⊢ ∃ y ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y
2 1 sepexi ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w z ∈ w ∧ w ∈ x