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 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑧𝑤𝑤𝑥 ) )

Proof

Step Hyp Ref Expression
1 ax-un 𝑦𝑧 ( ∃ 𝑤 ( 𝑧𝑤𝑤𝑥 ) → 𝑧𝑦 )
2 1 bm1.3ii 𝑦𝑧 ( 𝑧𝑦 ↔ ∃ 𝑤 ( 𝑧𝑤𝑤𝑥 ) )