This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Replacement Theorems requiring subset and intersection existence 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