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