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