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		df-ss	|- ( ~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 ) )