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 ) ) |
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 ) ) |