Metamath Proof Explorer


Theorem ssextss

Description: An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004)

Ref Expression
Assertion ssextss
|- ( A C_ B <-> A. x ( x C_ A -> x C_ B ) )

Proof

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