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 e. x

Proof

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