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	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ∈ V )
2		uniexr	⊢ ( ∪ 𝐴 ∈ V → 𝐴 ∈ V )
3	1 2	impbii	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )