Metamath Proof Explorer

Theorem elpwuni

Description: Relationship for power class and union. (Contributed by NM, 18-Jul-2006)

Ref Expression
Assertion elpwuni 
|- ( B e. A -> ( A C_ ~P B <-> U. A = B ) )

Proof

Step Hyp Ref Expression
1 sspwuni 
 |-  ( A C_ ~P B <-> U. A C_ B )
2 unissel 
 |-  ( ( U. A C_ B /\ B e. A ) -> U. A = B )
3 2 expcom 
 |-  ( B e. A -> ( U. A C_ B -> U. A = B ) )
4 eqimss 
 |-  ( U. A = B -> U. A C_ B )
5 3 4 impbid1 
 |-  ( B e. A -> ( U. A C_ B <-> U. A = B ) )
6 1 5 bitrid 
 |-  ( B e. A -> ( A C_ ~P B <-> U. A = B ) )