Theorem ax6e2eqVD 39143

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 38785) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 38773 is ax6e2eqVD 39143 without virtual deductions and was automatically derived from ax6e2eqVD 39143. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	|- (. A. x x = y ->. A. x x = y ).
2::	|- (. A. x x = y ,. x = u ->. x = u ).
3:1:	|- (. A. x x = y ->. x = y ).
4:2,3:	|- (. A. x x = y ,. x = u ->. y = u ).
5:2,4:	|- (. A. x x = y ,. x = u ->. ( x = u /\ y = u ) ).
6:5:	|- (. A. x x = y ->. ( x = u -> ( x = u /\ y = u ) ) ).
7:6:	|- ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
8:7:	|- ( A. x A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
9::	|- ( A. x x = y <-> A. x A. x x = y )
10:8,9:	|- ( A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
11:1,10:	|- (. A. x x = y ->. A. x ( x = u -> ( x = u /\ y = u ) ) ).
12:11:	|- (. A. x x = y ->. ( E. x x = u -> E. x ( x = u /\ y = u ) ) ).
13::	|- E. x x = u
14:13,12:	|- (. A. x x = y ->. E. x ( x = u /\ y = u ) ).
140:14:	|- ( A. x x = y -> E. x ( x = u /\ y = u ) )
141:140:	|- ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
15:1,141:	|- (. A. x x = y ->. A. x E. x ( x = u /\ y = u ) ).
16:1,15:	|- (. A. x x = y ->. A. y E. x ( x = u /\ y = u ) ).
17:16:	|- (. A. x x = y ->. E. y E. x ( x = u /\ y = u ) ).
18:17:	|- (. A. x x = y ->. E. x E. y ( x = u /\ y = u ) ).
19::	|- (. u = v ->. u = v ).
20::	|- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = u ) ).
21:20:	|- (. u = v ,. ( x = u /\ y = u ) ->. y = u ).
22:19,21:	|- (. u = v ,. ( x = u /\ y = u ) ->. y = v ).
23:20:	|- (. u = v ,. ( x = u /\ y = u ) ->. x = u ).
24:22,23:	|- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = v ) ).
25:24:	|- (. u = v ->. ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
26:25:	|- (. u = v ->. A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
27:26:	|- (. u = v ->. ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
28:27:	|- (. u = v ->. A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
29:28:	|- (. u = v ->. ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ).
30:29:	|- ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
31:18,30:	|- (. A. x x = y ->. ( u = v -> E. x E. y ( x = u /\ y = v ) ) ).
qed:31:	|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )

Assertion

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

Distinct variable groups:   x, u   y, u   x, v   y, v

Proof of Theorem ax6e2eqVD

Step	Hyp	Ref	Expression
1		idn1 38790	. . . . . 6 |- (. A. x x = y ->. A. x x = y ).
2		ax6ev 1890	. . . . . . . . . 10 |- E. x x = u
3		hba1 2151	. . . . . . . . . . . . . 14 |- ( A. x x = y -> A. x A. x x = y )
4		sp 2053	. . . . . . . . . . . . . 14 |- ( A. x A. x x = y -> A. x x = y )
5	3, 4	impbii 199	. . . . . . . . . . . . 13 |- ( A. x x = y <-> A. x A. x x = y )
6		idn2 38838	. . . . . . . . . . . . . . . . 17 |- (. A. x x = y ,. x = u ->. x = u ).
7		sp 2053	. . . . . . . . . . . . . . . . . . 19 |- ( A. x x = y -> x = y )
8	1, 7	e1a 38852	. . . . . . . . . . . . . . . . . 18 |- (. A. x x = y ->. x = y ).
9		ax7 1943	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x = u -> y = u ) )
10	9	com12 32	. . . . . . . . . . . . . . . . . 18 |- ( x = u -> ( x = y -> y = u ) )
11	6, 8, 10	e21 38957	. . . . . . . . . . . . . . . . 17 |- (. A. x x = y ,. x = u ->. y = u ).
12		pm3.2 463	. . . . . . . . . . . . . . . . 17 |- ( x = u -> ( y = u -> ( x = u /\ y = u ) ) )
13	6, 11, 12	e22 38896	. . . . . . . . . . . . . . . 16 |- (. A. x x = y ,. x = u ->. ( x = u /\ y = u ) ).
14	13	in2 38830	. . . . . . . . . . . . . . 15 |- (. A. x x = y ->. ( x = u -> ( x = u /\ y = u ) ) ).
15	14	in1 38787	. . . . . . . . . . . . . 14 |- ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
16	15	alimi 1739	. . . . . . . . . . . . 13 |- ( A. x A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
17	5, 16	sylbi 207	. . . . . . . . . . . 12 |- ( A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
18	1, 17	e1a 38852	. . . . . . . . . . 11 |- (. A. x x = y ->. A. x ( x = u -> ( x = u /\ y = u ) ) ).
19		exim 1761	. . . . . . . . . . 11 |- ( A. x ( x = u -> ( x = u /\ y = u ) ) -> ( E. x x = u -> E. x ( x = u /\ y = u ) ) )
20	18, 19	e1a 38852	. . . . . . . . . 10 |- (. A. x x = y ->. ( E. x x = u -> E. x ( x = u /\ y = u ) ) ).
21		pm2.27 42	. . . . . . . . . 10 |- ( E. x x = u -> ( ( E. x x = u -> E. x ( x = u /\ y = u ) ) -> E. x ( x = u /\ y = u ) ) )
22	2, 20, 21	e01 38916	. . . . . . . . 9 |- (. A. x x = y ->. E. x ( x = u /\ y = u ) ).
23	22	in1 38787	. . . . . . . 8 |- ( A. x x = y -> E. x ( x = u /\ y = u ) )
24	23	axc4i 2131	. . . . . . 7 |- ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
25	1, 24	e1a 38852	. . . . . 6 |- (. A. x x = y ->. A. x E. x ( x = u /\ y = u ) ).
26		axc11 2314	. . . . . 6 |- ( A. x x = y -> ( A. x E. x ( x = u /\ y = u ) -> A. y E. x ( x = u /\ y = u ) ) )
27	1, 25, 26	e11 38913	. . . . 5 |- (. A. x x = y ->. A. y E. x ( x = u /\ y = u ) ).
28		19.2 1892	. . . . 5 |- ( A. y E. x ( x = u /\ y = u ) -> E. y E. x ( x = u /\ y = u ) )
29	27, 28	e1a 38852	. . . 4 |- (. A. x x = y ->. E. y E. x ( x = u /\ y = u ) ).
30		excomim 2043	. . . 4 |- ( E. y E. x ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = u ) )
31	29, 30	e1a 38852	. . 3 |- (. A. x x = y ->. E. x E. y ( x = u /\ y = u ) ).
32		idn1 38790	. . . . . . . . . . 11 |- (. u = v ->. u = v ).
33		idn2 38838	. . . . . . . . . . . 12 |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = u ) ).
34		simpr 477	. . . . . . . . . . . 12 |- ( ( x = u /\ y = u ) -> y = u )
35	33, 34	e2 38856	. . . . . . . . . . 11 |- (. u = v ,. ( x = u /\ y = u ) ->. y = u ).
36		equtrr 1949	. . . . . . . . . . 11 |- ( u = v -> ( y = u -> y = v ) )
37	32, 35, 36	e12 38951	. . . . . . . . . 10 |- (. u = v ,. ( x = u /\ y = u ) ->. y = v ).
38		simpl 473	. . . . . . . . . . 11 |- ( ( x = u /\ y = u ) -> x = u )
39	33, 38	e2 38856	. . . . . . . . . 10 |- (. u = v ,. ( x = u /\ y = u ) ->. x = u ).
40		pm3.21 464	. . . . . . . . . 10 |- ( y = v -> ( x = u -> ( x = u /\ y = v ) ) )
41	37, 39, 40	e22 38896	. . . . . . . . 9 |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = v ) ).
42	41	in2 38830	. . . . . . . 8 |- (. u = v ->. ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
43	42	gen11 38841	. . . . . . 7 |- (. u = v ->. A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
44		exim 1761	. . . . . . 7 |- ( A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) -> ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) )
45	43, 44	e1a 38852	. . . . . 6 |- (. u = v ->. ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
46	45	gen11 38841	. . . . 5 |- (. u = v ->. A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
47		exim 1761	. . . . 5 |- ( A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
48	46, 47	e1a 38852	. . . 4 |- (. u = v ->. ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ).
49	48	in1 38787	. . 3 |- ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
50		pm2.04 90	. . . 4 |- ( ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ) -> ( E. x E. y ( x = u /\ y = u ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
51	50	com12 32	. . 3 |- ( E. x E. y ( x = u /\ y = u ) -> ( ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
52	31, 49, 51	e10 38919	. 2 |- (. A. x x = y ->. ( u = v -> E. x E. y ( x = u /\ y = v ) ) ).
53	52	in1 38787	1 |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)