Theorem nev

Description: Express that not every set is in a class. (Contributed by RP, 16-Apr-2020)

	Ref	Expression
Assertion	nev	$$⊢A\ne \mathrm{V}\leftrightarrow \neg \forall xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		eqv	$$⊢A=\mathrm{V}\leftrightarrow \forall xx\in A$$
2	1	necon3abii	$$⊢A\ne \mathrm{V}\leftrightarrow \neg \forall xx\in A$$