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

Metamath Proof Explorer

Theorem vnexOLD

Description: Obsolete proof of vnex as of 25-Apr-2026. (Contributed by NM, 4-Jul-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vnexOLD ⊢ ¬ ∃ x x = V

Proof

Step Hyp Ref Expression
1 nalset ⊢ ¬ ∃ x ∀ y y ∈ x
2 vex ⊢ y ∈ V
3 2 tbt ⊢ y ∈ x ↔ y ∈ x ↔ y ∈ V
4 3 albii ⊢ ∀ y y ∈ x ↔ ∀ y y ∈ x ↔ y ∈ V
5 dfcleq ⊢ x = V ↔ ∀ y y ∈ x ↔ y ∈ V
6 4 5 bitr4i ⊢ ∀ y y ∈ x ↔ x = V
7 6 exbii ⊢ ∃ x ∀ y y ∈ x ↔ ∃ x x = V
8 1 7 mtbi ⊢ ¬ ∃ x x = V