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

Metamath Proof Explorer

Theorem ax6e2eq

Description: Alternate form of ax6e for non-distinct x , y and u = v . ax6e2eq is derived from ax6e2eqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2eq 
|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )

Proof

Step Hyp Ref Expression
1 ax6ev 
 |-  E. x x = u
2 hbae 
 |-  ( A. x x = y -> A. x A. x x = y )
3 ax7 
 |-  ( x = y -> ( x = u -> y = u ) )
4 3 sps 
 |-  ( A. x x = y -> ( x = u -> y = u ) )
5 4 ancld 
 |-  ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
6 2 5 eximdh 
 |-  ( A. x x = y -> ( E. x x = u -> E. x ( x = u /\ y = u ) ) )
7 1 6 mpi 
 |-  ( A. x x = y -> E. x ( x = u /\ y = u ) )
8 7 axc4i 
 |-  ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
9 axc11 
 |-  ( A. x x = y -> ( A. x E. x ( x = u /\ y = u ) -> A. y E. x ( x = u /\ y = u ) ) )
10 8 9 mpd 
 |-  ( A. x x = y -> A. y E. x ( x = u /\ y = u ) )
11 19.2 
 |-  ( A. y E. x ( x = u /\ y = u ) -> E. y E. x ( x = u /\ y = u ) )
12 10 11 syl 
 |-  ( A. x x = y -> E. y E. x ( x = u /\ y = u ) )
13 excomim 
 |-  ( E. y E. x ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = u ) )
14 12 13 syl 
 |-  ( A. x x = y -> E. x E. y ( x = u /\ y = u ) )
15 equtrr 
 |-  ( u = v -> ( y = u -> y = v ) )
16 15 anim2d 
 |-  ( u = v -> ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) )
17 16 2eximdv 
 |-  ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
18 14 17 syl5com 
 |-  ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )