# 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$