Metamath Proof Explorer

Theorem sspwuni

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

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

Proof

Step Hyp Ref Expression
1 velpw 
 |-  ( x e. ~P B <-> x C_ B )
2 1 ralbii 
 |-  ( A. x e. A x e. ~P B <-> A. x e. A x C_ B )
3 dfss3 
 |-  ( A C_ ~P B <-> A. x e. A x e. ~P B )
4 unissb 
 |-  ( U. A C_ B <-> A. x e. A x C_ B )
5 2 3 4 3bitr4i 
 |-  ( A C_ ~P B <-> U. A C_ B )