Metamath Proof Explorer

Theorem pwnss

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 )

Proof

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 )