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 ¬ 𝑥 ∈ 𝑥

Proof

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