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

Proof

Step	Hyp	Ref	Expression
1		rru	$$⊢\neg \left\{x\in A|\neg x\in x\right\}\in A$$
2		ssel	$$⊢𝒫A\subseteq A\to \left(\left\{x\in A|\neg x\in x\right\}\in 𝒫A\to \left\{x\in A|\neg x\in x\right\}\in A\right)$$
3	1 2	mtoi	$$⊢𝒫A\subseteq A\to \neg \left\{x\in A|\neg x\in x\right\}\in 𝒫A$$
4		rabelpw	$$⊢A\in V\to \left\{x\in A|\neg x\in x\right\}\in 𝒫A$$
5	3 4	nsyl3	$$⊢A\in V\to \neg 𝒫A\subseteq A$$