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 , but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993)

Ref Expression
Assertion elirrv ⊢ ¬ x ∈ x

Proof

Step Hyp Ref Expression
1 snex ⊢ 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 syl5bi ⊢ 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