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)

Ref Expression
Assertion elirrv 
|- -. x e. x

Proof

Step Hyp Ref Expression
1 biimpr 
 |-  ( ( y e. w <-> y = x ) -> ( y = x -> y e. w ) )
2 1 alimi 
 |-  ( A. y ( y e. w <-> y = x ) -> A. y ( y = x -> y e. w ) )
3 elequ1 
 |-  ( y = x -> ( y e. w <-> x e. w ) )
4 3 equsalvw 
 |-  ( A. y ( y = x -> y e. w ) <-> x e. w )
5 2 4 sylib 
 |-  ( A. y ( y e. w <-> y = x ) -> x e. w )
6 3 equsexvw 
 |-  ( E. y ( y = x /\ y e. w ) <-> x e. w )
7 exsimpr 
 |-  ( E. y ( y = x /\ y e. w ) -> E. y y e. w )
8 6 7 sylbir 
 |-  ( x e. w -> E. y y e. w )
9 ax-reg 
 |-  ( E. y y e. w -> E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) )
10 8 9 syl 
 |-  ( x e. w -> E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) )
11 elequ1 
 |-  ( z = x -> ( z e. y <-> x e. y ) )
12 elequ1 
 |-  ( z = x -> ( z e. w <-> x e. w ) )
13 12 notbid 
 |-  ( z = x -> ( -. z e. w <-> -. x e. w ) )
14 11 13 imbi12d 
 |-  ( z = x -> ( ( z e. y -> -. z e. w ) <-> ( x e. y -> -. x e. w ) ) )
15 14 spvv 
 |-  ( A. z ( z e. y -> -. z e. w ) -> ( x e. y -> -. x e. w ) )
16 con2 
 |-  ( ( x e. y -> -. x e. w ) -> ( x e. w -> -. x e. y ) )
17 16 com12 
 |-  ( x e. w -> ( ( x e. y -> -. x e. w ) -> -. x e. y ) )
18 17 anim2d 
 |-  ( x e. w -> ( ( y e. w /\ ( x e. y -> -. x e. w ) ) -> ( y e. w /\ -. x e. y ) ) )
19 15 18 sylan2i 
 |-  ( x e. w -> ( ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) -> ( y e. w /\ -. x e. y ) ) )
20 19 eximdv 
 |-  ( x e. w -> ( E. y ( y e. w /\ A. z ( z e. y -> -. z e. w ) ) -> E. y ( y e. w /\ -. x e. y ) ) )
21 10 20 mpd 
 |-  ( x e. w -> E. y ( y e. w /\ -. x e. y ) )
22 19.29 
 |-  ( ( A. y ( y e. w <-> y = x ) /\ E. y ( y e. w /\ -. x e. y ) ) -> E. y ( ( y e. w <-> y = x ) /\ ( y e. w /\ -. x e. y ) ) )
23 biimp 
 |-  ( ( y e. w <-> y = x ) -> ( y e. w -> y = x ) )
24 23 anim1d 
 |-  ( ( y e. w <-> y = x ) -> ( ( y e. w /\ -. x e. y ) -> ( y = x /\ -. x e. y ) ) )
25 ax9v2 
 |-  ( x = y -> ( x e. x -> x e. y ) )
26 25 equcoms 
 |-  ( y = x -> ( x e. x -> x e. y ) )
27 26 con3dimp 
 |-  ( ( y = x /\ -. x e. y ) -> -. x e. x )
28 24 27 syl6 
 |-  ( ( y e. w <-> y = x ) -> ( ( y e. w /\ -. x e. y ) -> -. x e. x ) )
29 28 imp 
 |-  ( ( ( y e. w <-> y = x ) /\ ( y e. w /\ -. x e. y ) ) -> -. x e. x )
30 29 exlimiv 
 |-  ( E. y ( ( y e. w <-> y = x ) /\ ( y e. w /\ -. x e. y ) ) -> -. x e. x )
31 22 30 syl 
 |-  ( ( A. y ( y e. w <-> y = x ) /\ E. y ( y e. w /\ -. x e. y ) ) -> -. x e. x )
32 21 31 sylan2 
 |-  ( ( A. y ( y e. w <-> y = x ) /\ x e. w ) -> -. x e. x )
33 5 32 mpdan 
 |-  ( A. y ( y e. w <-> y = x ) -> -. x e. x )
34 el 
 |-  E. w x e. w
35 4 biimpri 
 |-  ( x e. w -> A. y ( y = x -> y e. w ) )
36 34 35 eximii 
 |-  E. w A. y ( y = x -> y e. w )
37 36 sepexi 
 |-  E. w A. y ( y e. w <-> y = x )
38 33 37 exlimiiv 
 |-  -. x e. x