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

Proof

Step	Hyp	Ref	Expression
1		snex	|- { x } e. _V
2		eleq1w	|- ( y = x -> ( y e. { x } <-> x e. { x } ) )
3		vsnid	|- x e. { x }
4	2 3	speivw	|- E. y y e. { x }
5		zfregcl	|- ( { x } e. _V -> ( E. y y e. { x } -> E. y e. { x } A. z e. y -. z e. { x } ) )
6	1 4 5	mp2	|- E. y e. { x } A. z e. y -. z e. { x }
7		velsn	|- ( y e. { x } <-> y = x )
8		ax9	|- ( x = y -> ( x e. x -> x e. y ) )
9	8	equcoms	|- ( y = x -> ( x e. x -> x e. y ) )
10	9	com12	|- ( x e. x -> ( y = x -> x e. y ) )
11	7 10	syl5bi	|- ( x e. x -> ( y e. { x } -> x e. y ) )
12		eleq1w	|- ( z = x -> ( z e. { x } <-> x e. { x } ) )
13	12	notbid	|- ( z = x -> ( -. z e. { x } <-> -. x e. { x } ) )
14	13	rspccv	|- ( A. z e. y -. z e. { x } -> ( x e. y -> -. x e. { x } ) )
15	3 14	mt2i	|- ( A. z e. y -. z e. { x } -> -. x e. y )
16	11 15	nsyli	|- ( x e. x -> ( A. z e. y -. z e. { x } -> -. y e. { x } ) )
17	16	con2d	|- ( x e. x -> ( y e. { x } -> -. A. z e. y -. z e. { x } ) )
18	17	ralrimiv	|- ( x e. x -> A. y e. { x } -. A. z e. y -. z e. { x } )
19		ralnex	|- ( A. y e. { x } -. A. z e. y -. z e. { x } <-> -. E. y e. { x } A. z e. y -. z e. { x } )
20	18 19	sylib	|- ( x e. x -> -. E. y e. { x } A. z e. y -. z e. { x } )
21	6 20	mt2	|- -. x e. x