Theorem ax6e2ndALT 39166

Description: If at least two sets exist (dtru 4857) , then the same is true expressed in an alternate form similar to the form of ax6e 2250. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 39144. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

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

Proof of Theorem ax6e2ndALT

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . . . 7 |- u e. _V
2		ax6e 2250	. . . . . . 7 |- E. y y = v
3	1, 2	pm3.2i 471	. . . . . 6 |- ( u e. _V /\ E. y y = v )
4		19.42v 1918	. . . . . . 7 |- ( E. y ( u e. _V /\ y = v ) <-> ( u e. _V /\ E. y y = v ) )
5	4	biimpri 218	. . . . . 6 |- ( ( u e. _V /\ E. y y = v ) -> E. y ( u e. _V /\ y = v ) )
6	3, 5	ax-mp 5	. . . . 5 |- E. y ( u e. _V /\ y = v )
7		isset 3207	. . . . . . 7 |- ( u e. _V <-> E. x x = u )
8	7	anbi1i 731	. . . . . 6 |- ( ( u e. _V /\ y = v ) <-> ( E. x x = u /\ y = v ) )
9	8	exbii 1774	. . . . 5 |- ( E. y ( u e. _V /\ y = v ) <-> E. y ( E. x x = u /\ y = v ) )
10	6, 9	mpbi 220	. . . 4 |- E. y ( E. x x = u /\ y = v )
11		id 22	. . . . . 6 |- ( -. A. x x = y -> -. A. x x = y )
12		hbnae 2317	. . . . . . 7 |- ( -. A. x x = y -> A. y -. A. x x = y )
13		hbn1 2020	. . . . . . . . . . . 12 |- ( -. A. x x = y -> A. x -. A. x x = y )
14		ax-5 1839	. . . . . . . . . . . . . . . 16 |- ( z = v -> A. x z = v )
15		ax-5 1839	. . . . . . . . . . . . . . . 16 |- ( y = v -> A. z y = v )
16		id 22	. . . . . . . . . . . . . . . . 17 |- ( z = y -> z = y )
17		equequ1 1952	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( z = v <-> y = v ) )
18	17	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( z = y -> z = y ) -> ( z = y -> ( z = v <-> y = v ) ) )
19	16, 18	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( z = y -> ( z = v <-> y = v ) )
20	14, 15, 19	dvelimh 2336	. . . . . . . . . . . . . . 15 |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
21	11, 20	syl 17	. . . . . . . . . . . . . 14 |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
22	21	idiALT 38683	. . . . . . . . . . . . 13 |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
23	22	alimi 1739	. . . . . . . . . . . 12 |- ( A. x -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
24	13, 23	syl 17	. . . . . . . . . . 11 |- ( -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
25	11, 24	syl 17	. . . . . . . . . 10 |- ( -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
26		19.41rg 38766	. . . . . . . . . 10 |- ( A. x ( y = v -> A. x y = v ) -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
27	25, 26	syl 17	. . . . . . . . 9 |- ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
28	27	idiALT 38683	. . . . . . . 8 |- ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
29	28	alimi 1739	. . . . . . 7 |- ( A. y -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
30	12, 29	syl 17	. . . . . 6 |- ( -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
31	11, 30	syl 17	. . . . 5 |- ( -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
32		exim 1761	. . . . 5 |- ( A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) -> ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) )
33	31, 32	syl 17	. . . 4 |- ( -. A. x x = y -> ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) )
34		pm3.35 611	. . . 4 |- ( ( E. y ( E. x x = u /\ y = v ) /\ ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) ) -> E. y E. x ( x = u /\ y = v ) )
35	10, 33, 34	sylancr 695	. . 3 |- ( -. A. x x = y -> E. y E. x ( x = u /\ y = v ) )
36		excomim 2043	. . 3 |- ( E. y E. x ( x = u /\ y = v ) -> E. x E. y ( x = u /\ y = v ) )
37	35, 36	syl 17	. 2 |- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
38	37	idiALT 38683	1 |- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200

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-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by: (None)