Metamath Proof Explorer

Theorem pwssb

Description: Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006)

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

Proof

Step Hyp Ref Expression
1 sspwuni 
 |-  ( A C_ ~P B <-> U. A C_ B )
2 unissb 
 |-  ( U. A C_ B <-> A. x e. A x C_ B )
3 1 2 bitri 
 |-  ( A C_ ~P B <-> A. x e. A x C_ B )