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 ⊢ ¬ x ∈ x

Proof

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