Theorem axregndlem1

Description: Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	axregndlem1	|- ( A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( x e. y -> E. x x e. y )
2		nfae	|- F/ x A. x x = z
3		nfae	|- F/ z A. x x = z
4		elirrv	|- -. x e. x
5		elequ1	|- ( x = z -> ( x e. x <-> z e. x ) )
6	4 5	mtbii	|- ( x = z -> -. z e. x )
7	6	sps	|- ( A. x x = z -> -. z e. x )
8	7	pm2.21d	|- ( A. x x = z -> ( z e. x -> -. z e. y ) )
9	3 8	alrimi	|- ( A. x x = z -> A. z ( z e. x -> -. z e. y ) )
10	9	anim2i	|- ( ( x e. y /\ A. x x = z ) -> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )
11	10	expcom	|- ( A. x x = z -> ( x e. y -> ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
12	2 11	eximd	|- ( A. x x = z -> ( E. x x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
13	1 12	syl5	|- ( A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )