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

Metamath Proof Explorer

Theorem elirrvOLD

Description: Obsolete version of elirrv as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elirrvOLD ⊢ ¬ x ∈ x

Proof

Step Hyp Ref Expression
1 vsnex ⊢ x ∈ V
2 eleq1w ⊢ y = x → y ∈ x ↔ x ∈ x
3 vsnid ⊢ x ∈ x
4 2 3 speivw ⊢ ∃ y y ∈ x
5 zfregcl ⊢ x ∈ V → ∃ y y ∈ x → ∃ y ∈ x ∀ z ∈ y ¬ z ∈ x
6 1 4 5 mp2 ⊢ ∃ y ∈ x ∀ z ∈ y ¬ z ∈ x
7 velsn ⊢ y ∈ x ↔ y = x
8 ax9 ⊢ x = y → x ∈ x → x ∈ y
9 8 equcoms ⊢ y = x → x ∈ x → x ∈ y
10 9 com12 ⊢ x ∈ x → y = x → x ∈ y
11 7 10 biimtrid ⊢ x ∈ x → y ∈ x → x ∈ y
12 eleq1w ⊢ z = x → z ∈ x ↔ x ∈ x
13 12 notbid ⊢ z = x → ¬ z ∈ x ↔ ¬ x ∈ x
14 13 rspccv ⊢ ∀ z ∈ y ¬ z ∈ x → x ∈ y → ¬ x ∈ x
15 3 14 mt2i ⊢ ∀ z ∈ y ¬ z ∈ x → ¬ x ∈ y
16 11 15 nsyli ⊢ x ∈ x → ∀ z ∈ y ¬ z ∈ x → ¬ y ∈ x
17 16 con2d ⊢ x ∈ x → y ∈ x → ¬ ∀ z ∈ y ¬ z ∈ x
18 17 ralrimiv ⊢ x ∈ x → ∀ y ∈ x ¬ ∀ z ∈ y ¬ z ∈ x
19 ralnex ⊢ ∀ y ∈ x ¬ ∀ z ∈ y ¬ z ∈ x ↔ ¬ ∃ y ∈ x ∀ z ∈ y ¬ z ∈ x
20 18 19 sylib ⊢ x ∈ x → ¬ ∃ y ∈ x ∀ z ∈ y ¬ z ∈ x
21 6 20 mt2 ⊢ ¬ x ∈ x