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