Metamath Proof Explorer


Theorem uniex

Description: The Axiom of Union in class notation. This says that if A is a set i.e. A e. _V (see isset ), then the union of A is also a set. Same as Axiom 3 of TakeutiZaring p. 16. (Contributed by NM, 11-Aug-1993)

Ref Expression
Hypothesis uniex.1 A V
Assertion uniex A V

Proof

Step Hyp Ref Expression
1 uniex.1 A V
2 uniexg A V A V
3 1 2 ax-mp A V