Theorem ax6e2ndeq 38775

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. ax6e2ndeq 38775 is derived from ax6e2ndeqVD 39145. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

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	2, 3	pm2.61i 176	. . 3 |- ( u = v -> E. x E. y ( x = u /\ y = v ) )
5	1, 4	jaoi 394	. 2 |- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
6		olc 399	. . . 4 |- ( u = v -> ( -. A. x x = y \/ u = v ) )
7	6	a1d 25	. . 3 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
8		excom 2042	. . . . . 6 |- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
9		neeq1 2856	. . . . . . . . . . . . 13 |- ( x = u -> ( x =/= v <-> u =/= v ) )
10	9	biimprcd 240	. . . . . . . . . . . 12 |- ( u =/= v -> ( x = u -> x =/= v ) )
11	10	adantrd 484	. . . . . . . . . . 11 |- ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= v ) )
12		simpr 477	. . . . . . . . . . . 12 |- ( ( x = u /\ y = v ) -> y = v )
13	12	a1i 11	. . . . . . . . . . 11 |- ( u =/= v -> ( ( x = u /\ y = v ) -> y = v ) )
14		neeq2 2857	. . . . . . . . . . . 12 |- ( y = v -> ( x =/= y <-> x =/= v ) )
15	14	biimprcd 240	. . . . . . . . . . 11 |- ( x =/= v -> ( y = v -> x =/= y ) )
16	11, 13, 15	syl6c 70	. . . . . . . . . 10 |- ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= y ) )
17		sp 2053	. . . . . . . . . . 11 |- ( A. x x = y -> x = y )
18	17	necon3ai 2819	. . . . . . . . . 10 |- ( x =/= y -> -. A. x x = y )
19	16, 18	syl6 35	. . . . . . . . 9 |- ( u =/= v -> ( ( x = u /\ y = v ) -> -. A. x x = y ) )
20	19	eximdv 1846	. . . . . . . 8 |- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
21		nfnae 2318	. . . . . . . . 9 |- F/ x -. A. x x = y
22	21	19.9 2072	. . . . . . . 8 |- ( E. x -. A. x x = y <-> -. A. x x = y )
23	20, 22	syl6ib 241	. . . . . . 7 |- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
24	23	eximdv 1846	. . . . . 6 |- ( u =/= v -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
25	8, 24	syl5bi 232	. . . . 5 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
26		nfnae 2318	. . . . . 6 |- F/ y -. A. x x = y
27	26	19.9 2072	. . . . 5 |- ( E. y -. A. x x = y <-> -. A. x x = y )
28	25, 27	syl6ib 241	. . . 4 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) )
29		orc 400	. . . 4 |- ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
30	28, 29	syl6 35	. . 3 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
31	7, 30	pm2.61ine 2877	. 2 |- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
32	5, 31	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-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:  2sb5nd  38776  2uasbanh  38777  2sb5ndVD  39146  2uasbanhVD  39147  2sb5ndALT  39168