Theorem prcnel

Description: A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020) (Proof shortened by AV, 14-Nov-2020)

	Ref	Expression
Assertion	prcnel	$$⊢\neg A\in \mathrm{V}\to \neg A\in V$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2	1	con3i	$$⊢\neg A\in \mathrm{V}\to \neg A\in V$$