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