Metamath Proof Explorer

Theorem uniexr

Description: Converse of the Axiom of Union. Note that it does not require ax-un . (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion uniexr 
|- ( U. A e. V -> A e. _V )

Proof

Step Hyp Ref Expression
1 pwuni 
 |-  A C_ ~P U. A
2 pwexg 
 |-  ( U. A e. V -> ~P U. A e. _V )
3 ssexg 
 |-  ( ( A C_ ~P U. A /\ ~P U. A e. _V ) -> A e. _V )
4 1 2 3 sylancr 
 |-  ( U. A e. V -> A e. _V )