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\in V\to 𝒫A\ne A$$

Proof

Step	Hyp	Ref	Expression
1		pwnss	$$⊢A\in V\to \neg 𝒫A\subseteq A$$
2		eqimss	$$⊢𝒫A=A\to 𝒫A\subseteq A$$
3	2	necon3bi	$$⊢\neg 𝒫A\subseteq A\to 𝒫A\ne A$$
4	1 3	syl	$$⊢A\in V\to 𝒫A\ne A$$