Metamath Proof Explorer


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 )