Theorem vneqv

Description: The universal class is not equal to any setvar. (Contributed by NM, 4-Jul-2005) Extract from vnex and shorten proof. (Revised by BJ, 25-Apr-2026)

	Ref	Expression
Assertion	vneqv	⊢ ¬ 𝑥 = V

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		eleq2	⊢ ( 𝑥 = V → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ V ) )
3	1 2	mpbiri	⊢ ( 𝑥 = V → 𝑦 ∈ 𝑥 )
4	3	con3i	⊢ ( ¬ 𝑦 ∈ 𝑥 → ¬ 𝑥 = V )
5		exnelv	⊢ ∃ 𝑦 ¬ 𝑦 ∈ 𝑥
6	4 5	exlimiiv	⊢ ¬ 𝑥 = V