Metamath Proof Explorer


Theorem pwss

Description: Subclass relationship for power class. (Contributed by NM, 21-Jun-2009)

Ref Expression
Assertion pwss
|- ( ~P A C_ B <-> A. x ( x C_ A -> x e. B ) )

Proof

Step Hyp Ref Expression
1 dfss2
 |-  ( ~P A C_ B <-> A. x ( x e. ~P A -> x e. B ) )
2 velpw
 |-  ( x e. ~P A <-> x C_ A )
3 2 imbi1i
 |-  ( ( x e. ~P A -> x e. B ) <-> ( x C_ A -> x e. B ) )
4 3 albii
 |-  ( A. x ( x e. ~P A -> x e. B ) <-> A. x ( x C_ A -> x e. B ) )
5 1 4 bitri
 |-  ( ~P A C_ B <-> A. x ( x C_ A -> x e. B ) )