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