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

Metamath Proof Explorer

Theorem elirrv

Description: The membership relation is irreflexive: no set is a member of itself. Theorem 105 of Suppes p. 54. This is trivial to prove from zfregfr and efrirr (see elirrvALT ), but this proof is direct from ax-reg . (Contributed by NM, 19-Aug-1993) Reduce axiom dependencies and make use of ax-reg directly. (Revised by BTernaryTau, 27-Dec-2025) Avoid ax-pr . (Revised by BTernaryTau, 21-May-2026) (Proof shortened by Matthew House, 23-May-2026)

Ref Expression
Assertion elirrv ¬ 𝑥 ∈ 𝑥

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥 ) )
2 1 biimprcd ⊢ ( 𝑥 ∈ 𝑥 → ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑥 ) )
3 2 pm4.71rd ⊢ ( 𝑥 ∈ 𝑥 → ( 𝑧 = 𝑥 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) )
4 3 bibi2d ⊢ ( 𝑥 ∈ 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) ) )
5 4 albidv ⊢ ( 𝑥 ∈ 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) ) )
6 5 biimprcd ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ( 𝑥 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ) )
7 ax6ev ⊢ ∃ 𝑧 𝑧 = 𝑥
8 exbi ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∃ 𝑧 𝑧 ∈ 𝑦 ↔ ∃ 𝑧 𝑧 = 𝑥 ) )
9 7 8 mpbiri ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 𝑧 ∈ 𝑦 )
10 ax-reg ⊢ ( ∃ 𝑧 𝑧 ∈ 𝑦 → ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) )
11 9 10 syl ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) )
12 biimp ⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( 𝑧 ∈ 𝑦 → 𝑧 = 𝑥 ) )
13 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧 ) )
14 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
15 14 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦 ) ) )
17 16 spvv ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑦 ) )
18 17 con2d ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑧 ) )
19 12 18 anim12ii ⊢ ( ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
20 19 ex ⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑦 → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) ) )
21 20 impcomd ⊢ ( ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
22 21 aleximi ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ( ∃ 𝑧 ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) )
23 11 22 mpd ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) )
24 elequ12 ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑧 = 𝑥 ) → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥 ) )
25 24 anidms ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑥 ) )
26 25 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑥 ) )
27 26 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ↔ ¬ 𝑥 ∈ 𝑥 )
28 23 27 sylib ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥 ) → ¬ 𝑥 ∈ 𝑥 )
29 6 28 syl6 ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ( 𝑥 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑥 ) )
30 29 pm2.01d ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) ) → ¬ 𝑥 ∈ 𝑥 )
31 axsepg ⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 = 𝑥 ) )
32 30 31 exlimiiv ⊢ ¬ 𝑥 ∈ 𝑥