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 
|- ( A e. _V <-> U. A e. _V )

Proof

Step Hyp Ref Expression
1 uniexg 
 |-  ( A e. _V -> U. A e. _V )
2 uniexr 
 |-  ( U. A e. _V -> A e. _V )
3 1 2 impbii 
 |-  ( A e. _V <-> U. A e. _V )