Theorem nev

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

	Ref	Expression
Assertion	nev	⊢ ( 𝐴 ≠ V ↔ ¬ ∀ 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqv	⊢ ( 𝐴 = V ↔ ∀ 𝑥 𝑥 ∈ 𝐴 )
2	1	necon3abii	⊢ ( 𝐴 ≠ V ↔ ¬ ∀ 𝑥 𝑥 ∈ 𝐴 )