Theorem ax6e2ndeqALT 39167

Description: "At least two sets exist" expressed in the form of dtru 4857 is logically equivalent to the same expressed in a form similar to ax6e 2250 if dtru 4857 is false implies u = v. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD 39145. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax6e2ndeqALT	|- ( ( -. 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 ax6e2ndeqALT

Step	Hyp	Ref	Expression
1		ax6e2nd 38774	. . 3 |- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
2		ax6e2eq 38773	. . . 4 |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
3	1	a1d 25	. . . 4 |- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
4		exmid 431	. . . 4 |- ( A. x x = y \/ -. A. x x = y )
5		jao 534	. . . . 5 |- ( ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) -> ( ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) -> ( ( A. x x = y \/ -. A. x x = y ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) ) )
6	5	3imp 1256	. . . 4 |- ( ( ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) /\ ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) /\ ( A. x x = y \/ -. A. x x = y ) ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
7	2, 3, 4, 6	mp3an 1424	. . 3 |- ( u = v -> E. x E. y ( x = u /\ y = v ) )
8	1, 7	jaoi 394	. 2 |- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
9		hbnae 2317	. . . . . . . . 9 |- ( -. A. x x = y -> A. y -. A. x x = y )
10	9	eximi 1762	. . . . . . . 8 |- ( E. y -. A. x x = y -> E. y A. y -. A. x x = y )
11		nfa1 2028	. . . . . . . . 9 |- F/ y A. y -. A. x x = y
12	11	19.9 2072	. . . . . . . 8 |- ( E. y A. y -. A. x x = y <-> A. y -. A. x x = y )
13	10, 12	sylib 208	. . . . . . 7 |- ( E. y -. A. x x = y -> A. y -. A. x x = y )
14		sp 2053	. . . . . . 7 |- ( A. y -. A. x x = y -> -. A. x x = y )
15	13, 14	syl 17	. . . . . 6 |- ( E. y -. A. x x = y -> -. A. x x = y )
16		excom 2042	. . . . . . 7 |- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
17		nfa1 2028	. . . . . . . . . . . 12 |- F/ x A. x x = y
18	17	nfn 1784	. . . . . . . . . . 11 |- F/ x -. A. x x = y
19	18	19.9 2072	. . . . . . . . . 10 |- ( E. x -. A. x x = y <-> -. A. x x = y )
20		id 22	. . . . . . . . . . . . . . . 16 |- ( u =/= v -> u =/= v )
21		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> ( x = u /\ y = v ) )
22		simpl 473	. . . . . . . . . . . . . . . . 17 |- ( ( x = u /\ y = v ) -> x = u )
23	21, 22	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> x = u )
24		pm13.181 2876	. . . . . . . . . . . . . . . . 17 |- ( ( x = u /\ u =/= v ) -> x =/= v )
25	24	ancoms 469	. . . . . . . . . . . . . . . 16 |- ( ( u =/= v /\ x = u ) -> x =/= v )
26	20, 23, 25	syl2an2r 876	. . . . . . . . . . . . . . 15 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> x =/= v )
27		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( x = u /\ y = v ) -> y = v )
28	21, 27	syl 17	. . . . . . . . . . . . . . 15 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> y = v )
29		neeq2 2857	. . . . . . . . . . . . . . . 16 |- ( y = v -> ( x =/= y <-> x =/= v ) )
30	29	biimparc 504	. . . . . . . . . . . . . . 15 |- ( ( x =/= v /\ y = v ) -> x =/= y )
31	26, 28, 30	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> x =/= y )
32		df-ne 2795	. . . . . . . . . . . . . . . 16 |- ( x =/= y <-> -. x = y )
33	32	bicomi 214	. . . . . . . . . . . . . . 15 |- ( -. x = y <-> x =/= y )
34		sp 2053	. . . . . . . . . . . . . . . 16 |- ( A. x x = y -> x = y )
35	34	con3i 150	. . . . . . . . . . . . . . 15 |- ( -. x = y -> -. A. x x = y )
36	33, 35	sylbir 225	. . . . . . . . . . . . . 14 |- ( x =/= y -> -. A. x x = y )
37	31, 36	syl 17	. . . . . . . . . . . . 13 |- ( ( u =/= v /\ ( x = u /\ y = v ) ) -> -. A. x x = y )
38	37	ex 450	. . . . . . . . . . . 12 |- ( u =/= v -> ( ( x = u /\ y = v ) -> -. A. x x = y ) )
39	38	alrimiv 1855	. . . . . . . . . . 11 |- ( u =/= v -> A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) )
40		exim 1761	. . . . . . . . . . 11 |- ( A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
41	39, 40	syl 17	. . . . . . . . . 10 |- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
42		imbi2 338	. . . . . . . . . . 11 |- ( ( E. x -. A. x x = y <-> -. A. x x = y ) -> ( ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) <-> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ) )
43	42	biimpa 501	. . . . . . . . . 10 |- ( ( ( E. x -. A. x x = y <-> -. A. x x = y ) /\ ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) ) -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
44	19, 41, 43	sylancr 695	. . . . . . . . 9 |- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
45	44	alrimiv 1855	. . . . . . . 8 |- ( u =/= v -> A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
46		exim 1761	. . . . . . . 8 |- ( A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
47	45, 46	syl 17	. . . . . . 7 |- ( u =/= v -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
48		imbi1 337	. . . . . . . 8 |- ( ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) ) -> ( ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) <-> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ) )
49	48	biimpar 502	. . . . . . 7 |- ( ( ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) ) /\ ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ) -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
50	16, 47, 49	sylancr 695	. . . . . 6 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
51		pm3.34 610	. . . . . 6 |- ( ( ( E. y -. A. x x = y -> -. A. x x = y ) /\ ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ) -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) )
52	15, 50, 51	sylancr 695	. . . . 5 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) )
53		orc 400	. . . . . 6 |- ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
54	53	imim2i 16	. . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
55	52, 54	syl 17	. . . 4 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
56	55	idiALT 38683	. . 3 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
57		id 22	. . . . . 6 |- ( u = v -> u = v )
58		ax-1 6	. . . . . 6 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> u = v ) )
59	57, 58	syl 17	. . . . 5 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> u = v ) )
60		olc 399	. . . . . 6 |- ( u = v -> ( -. A. x x = y \/ u = v ) )
61	60	imim2i 16	. . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) -> u = v ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
62	59, 61	syl 17	. . . 4 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
63	62	idiALT 38683	. . 3 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
64		exmidne 2804	. . 3 |- ( u = v \/ u =/= v )
65		jao 534	. . . 4 |- ( ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u = v \/ u =/= v ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) ) )
66	65	3imp21 1277	. . 3 |- ( ( ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) /\ ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) /\ ( u = v \/ u =/= v ) ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
67	56, 63, 64, 66	mp3an 1424	. 2 |- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
68	8, 67	impbii 199	1 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   =/= wne 2794

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-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-v 3202

This theorem is referenced by: (None)