Description: The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | pwnss | |- ( A e. V -> -. ~P A C_ A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rru | |- -. { x e. A | -. x e. x } e. A |
|
2 | ssel | |- ( ~P A C_ A -> ( { x e. A | -. x e. x } e. ~P A -> { x e. A | -. x e. x } e. A ) ) |
|
3 | 1 2 | mtoi | |- ( ~P A C_ A -> -. { x e. A | -. x e. x } e. ~P A ) |
4 | ssrab2 | |- { x e. A | -. x e. x } C_ A |
|
5 | elpw2g | |- ( A e. V -> ( { x e. A | -. x e. x } e. ~P A <-> { x e. A | -. x e. x } C_ A ) ) |
|
6 | 4 5 | mpbiri | |- ( A e. V -> { x e. A | -. x e. x } e. ~P A ) |
7 | 3 6 | nsyl3 | |- ( A e. V -> -. ~P A C_ A ) |