Metamath Proof Explorer


Theorem pwnss

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 )

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