This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )