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 unieq x = A x = A
3 2 eleq1d x = A x V A V
4 uniex2 y y = x
5 4 issetri x V
6 1 3 5 vtocl A V