Metamath Proof Explorer


Theorem pwne

Description: No set equals its power set. The sethood antecedent is necessary; compare pwv . (Contributed by NM, 17-Nov-2008) (Proof shortened by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion pwne
|- ( A e. V -> ~P A =/= A )

Proof

Step Hyp Ref Expression
1 pwnss
 |-  ( A e. V -> -. ~P A C_ A )
2 eqimss
 |-  ( ~P A = A -> ~P A C_ A )
3 2 necon3bi
 |-  ( -. ~P A C_ A -> ~P A =/= A )
4 1 3 syl
 |-  ( A e. V -> ~P A =/= A )