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	⊢ 𝐴 ∈ V
Assertion	uniex	⊢ ∪ 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		uniex.1	⊢ 𝐴 ∈ V
2		uniexg	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ∈ V )
3	1 2	ax-mp	⊢ ∪ 𝐴 ∈ V