This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vnex

Description: The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005) (Proof shortened by BJ, 25-Apr-2026)

Ref Expression
Assertion vnex ¬ ∃ 𝑥 𝑥 = V

Proof

Step Hyp Ref Expression
1 vneqv ⊢ ¬ 𝑥 = V
2 1 nex ⊢ ¬ ∃ 𝑥 𝑥 = V