Theorem uniexb

Description: The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003)

	Ref	Expression
Assertion	uniexb	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢A\in \mathrm{V}\to \bigcup A\in \mathrm{V}$$
2		uniexr	$$⊢\bigcup A\in \mathrm{V}\to A\in \mathrm{V}$$
3	1 2	impbii	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$