Description: The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015) (Proof shortened by BJ, 24-Jul-2025)
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 | rabelpw | |- ( A e. V -> { x e. A | -. x e. x } e. ~P A ) |
|
5 | 3 4 | nsyl3 | |- ( A e. V -> -. ~P A C_ A ) |