Theorem eufromeq6 3833

Description: Two ways of expressing existential uniqueness via an indirect equality. The converse does not hold. Note that U.A = |^|A means A is a singleton (uniintsn 3253).

Assertion

Ref	Expression
eufromeq6	|- ((U.A =/= |^|A \/ B =/= (/)) -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))

Distinct variable groups:   x,y,A   x,B,y   x,C

Proof of Theorem eufromeq6

Step	Hyp	Ref	Expression
1		raleq 2266	. . . . . . 7 |- (B = (/) -> (A.y e. B x = C <-> A.y e. (/) x = C))
2	1	reubidv 2260	. . . . . 6 |- (B = (/) -> (E!x e. A A.y e. B x = C <-> E!x e. A A.y e. (/) x = C))
3		df-reu 2111	. . . . . . 7 |- (E!x e. A A.y e. (/) x = C <-> E!x(x e. A /\ A.y e. (/) x = C))
4		uniintsn 3253	. . . . . . . 8 |- (U.A = |^|A <-> E.x A = {x})
5		eusn 3096	. . . . . . . 8 |- (E!x x e. A <-> E.x A = {x})
6		ral0 2974	. . . . . . . . . 10 |- A.y e. (/) x = C
7	6	biantru 793	. . . . . . . . 9 |- (x e. A <-> (x e. A /\ A.y e. (/) x = C))
8	7	eubii 1780	. . . . . . . 8 |- (E!x x e. A <-> E!x(x e. A /\ A.y e. (/) x = C))
9	4, 5, 8	3bitr2i 196	. . . . . . 7 |- (U.A = |^|A <-> E!x(x e. A /\ A.y e. (/) x = C))
10	3, 9	bitr4i 193	. . . . . 6 |- (E!x e. A A.y e. (/) x = C <-> U.A = |^|A)
11	2, 10	syl6bb 595	. . . . 5 |- (B = (/) -> (E!x e. A A.y e. B x = C <-> U.A = |^|A))
12	11	necon3bbid 2034	. . . 4 |- (B = (/) -> (-. E!x e. A A.y e. B x = C <-> U.A =/= |^|A))
13		pm2.21 92	. . . 4 |- (-. E!x e. A A.y e. B x = C -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))
14	12, 13	syl6bir 232	. . 3 |- (B = (/) -> (U.A =/= |^|A -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C)))
15		eqeq1 1890	. . . . . . . 8 |- (x = z -> (x = C <-> z = C))
16	15	rexbidv 2124	. . . . . . 7 |- (x = z -> (E.y e. B x = C <-> E.y e. B z = C))
17	16	reu4 2446	. . . . . 6 |- (E!x e. A E.y e. B x = C <-> (E.x e. A E.y e. B x = C /\ A.x e. A A.z e. A ((E.y e. B x = C /\ E.y e. B z = C) -> x = z)))
18		reurex 2440	. . . . . . . 8 |- (E!x e. A A.y e. B x = C -> E.x e. A A.y e. B x = C)
19	18	adantl 424	. . . . . . 7 |- ((B =/= (/) /\ E!x e. A A.y e. B x = C) -> E.x e. A A.y e. B x = C)
20		r19.2z 2958	. . . . . . . . . 10 |- ((B =/= (/) /\ A.y e. B x = C) -> E.y e. B x = C)
21	20	ex 402	. . . . . . . . 9 |- (B =/= (/) -> (A.y e. B x = C -> E.y e. B x = C))
22	21	reximdv 2202	. . . . . . . 8 |- (B =/= (/) -> (E.x e. A A.y e. B x = C -> E.x e. A E.y e. B x = C))
23	22	adantr 425	. . . . . . 7 |- ((B =/= (/) /\ E!x e. A A.y e. B x = C) -> (E.x e. A A.y e. B x = C -> E.x e. A E.y e. B x = C))
24	19, 23	mpd 29	. . . . . 6 |- ((B =/= (/) /\ E!x e. A A.y e. B x = C) -> E.x e. A E.y e. B x = C)
25		hbreu1 2252	. . . . . . . 8 |- (E!x e. A A.y e. B x = C -> A.xE!x e. A A.y e. B x = C)
26	15	ralbidv 2123	. . . . . . . . . . . . . . . 16 |- (x = z -> (A.y e. B x = C <-> A.y e. B z = C))
27		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (v e. x -> A.y v e. x)
28		hbra1 2147	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. B z = C -> A.yA.y e. B z = C)
29		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (v e. A -> A.y v e. A)
30	28, 29	hbrab 2258	. . . . . . . . . . . . . . . . . . 19 |- (v e. {z e. A | A.y e. B z = C} -> A.y v e. {z e. A | A.y e. B z = C})
31	30	hbuni 3183	. . . . . . . . . . . . . . . . . 18 |- (v e. U.{z e. A | A.y e. B z = C} -> A.y v e. U.{z e. A | A.y e. B z = C})
32	27, 31	hbeq 1995	. . . . . . . . . . . . . . . . 17 |- (x = U.{z e. A | A.y e. B z = C} -> A.y x = U.{z e. A | A.y e. B z = C})
33		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (x = U.{z e. A | A.y e. B z = C} -> (x = C <-> U.{z e. A | A.y e. B z = C} = C))
34	32, 33	ralbid 2121	. . . . . . . . . . . . . . . 16 |- (x = U.{z e. A | A.y e. B z = C} -> (A.y e. B x = C <-> A.y e. B U.{z e. A | A.y e. B z = C} = C))
35	26, 34	reuuni3 3812	. . . . . . . . . . . . . . 15 |- (E!x e. A A.y e. B x = C -> A.y e. B U.{z e. A | A.y e. B z = C} = C)
36		anidm 478	. . . . . . . . . . . . . . 15 |- ((A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.y e. B U.{z e. A | A.y e. B z = C} = C) <-> A.y e. B U.{z e. A | A.y e. B z = C} = C)
37	35, 36	sylibr 217	. . . . . . . . . . . . . 14 |- (E!x e. A A.y e. B x = C -> (A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.y e. B U.{z e. A | A.y e. B z = C} = C))
38		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (U.{z e. A | A.y e. B z = C} = C -> A.wU.{z e. A | A.y e. B z = C} = C)
39		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
40		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (v e. w -> A.y v e. w)
41	39, 40	hbcsb1 2568	. . . . . . . . . . . . . . . . . 18 |- (v e. [_w / y]_C -> A.y v e. [_w / y]_C)
42	31, 41	hbeq 1995	. . . . . . . . . . . . . . . . 17 |- (U.{z e. A | A.y e. B z = C} = [_w / y]_C -> A.yU.{z e. A | A.y e. B z = C} = [_w / y]_C)
43	38, 42	raaan 2976	. . . . . . . . . . . . . . . 16 |- (A.y e. B A.w e. B (U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) <-> (A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.w e. B U.{z e. A | A.y e. B z = C} = [_w / y]_C))
44		csbeq1a 2546	. . . . . . . . . . . . . . . . . . 19 |- (y = w -> C = [_w / y]_C)
45	44	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (y = w -> (U.{z e. A | A.y e. B z = C} = C <-> U.{z e. A | A.y e. B z = C} = [_w / y]_C))
46	38, 42, 45	cbvral 2278	. . . . . . . . . . . . . . . . 17 |- (A.y e. B U.{z e. A | A.y e. B z = C} = C <-> A.w e. B U.{z e. A | A.y e. B z = C} = [_w / y]_C)
47	46	anbi2i 538	. . . . . . . . . . . . . . . 16 |- ((A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.y e. B U.{z e. A | A.y e. B z = C} = C) <-> (A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.w e. B U.{z e. A | A.y e. B z = C} = [_w / y]_C))
48	43, 47	bitr4i 193	. . . . . . . . . . . . . . 15 |- (A.y e. B A.w e. B (U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) <-> (A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.y e. B U.{z e. A | A.y e. B z = C} = C))
49		eqeq12 1896	. . . . . . . . . . . . . . . . . 18 |- ((x = C /\ z = [_w / y]_C) -> (x = z <-> C = [_w / y]_C))
50		eqtr2 1905	. . . . . . . . . . . . . . . . . 18 |- ((U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) -> C = [_w / y]_C)
51	49, 50	syl5cbir 228	. . . . . . . . . . . . . . . . 17 |- ((U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) -> ((x = C /\ z = [_w / y]_C) -> x = z))
52	51	ralimi 2168	. . . . . . . . . . . . . . . 16 |- (A.w e. B (U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) -> A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z))
53	52	ralimi 2168	. . . . . . . . . . . . . . 15 |- (A.y e. B A.w e. B (U.{z e. A | A.y e. B z = C} = C /\ U.{z e. A | A.y e. B z = C} = [_w / y]_C) -> A.y e. B A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z))
54	48, 53	sylbir 218	. . . . . . . . . . . . . 14 |- ((A.y e. B U.{z e. A | A.y e. B z = C} = C /\ A.y e. B U.{z e. A | A.y e. B z = C} = C) -> A.y e. B A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z))
55	37, 54	syl 12	. . . . . . . . . . . . 13 |- (E!x e. A A.y e. B x = C -> A.y e. B A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z))
56		r19.23v 2208	. . . . . . . . . . . . . . 15 |- (A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z) <-> (E.w e. B (x = C /\ z = [_w / y]_C) -> x = z))
57	56	ralbii 2127	. . . . . . . . . . . . . 14 |- (A.y e. B A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z) <-> A.y e. B (E.w e. B (x = C /\ z = [_w / y]_C) -> x = z))
58		r19.23v 2208	. . . . . . . . . . . . . 14 |- (A.y e. B (E.w e. B (x = C /\ z = [_w / y]_C) -> x = z) <-> (E.y e. B E.w e. B (x = C /\ z = [_w / y]_C) -> x = z))
59	57, 58	bitri 190	. . . . . . . . . . . . 13 |- (A.y e. B A.w e. B ((x = C /\ z = [_w / y]_C) -> x = z) <-> (E.y e. B E.w e. B (x = C /\ z = [_w / y]_C) -> x = z))
60	55, 59	sylib 215	. . . . . . . . . . . 12 |- (E!x e. A A.y e. B x = C -> (E.y e. B E.w e. B (x = C /\ z = [_w / y]_C) -> x = z))
61		ax-17 1317	. . . . . . . . . . . . . 14 |- (x = C -> A.w x = C)
62		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (z e. w -> A.y z e. w)
63	39, 62	hbcsb1 2568	. . . . . . . . . . . . . . 15 |- (z e. [_w / y]_C -> A.y z e. [_w / y]_C)
64	63	hbeleq 1997	. . . . . . . . . . . . . 14 |- (z = [_w / y]_C -> A.y z = [_w / y]_C)
65	61, 64	reean 2247	. . . . . . . . . . . . 13 |- (E.y e. B E.w e. B (x = C /\ z = [_w / y]_C) <-> (E.y e. B x = C /\ E.w e. B z = [_w / y]_C))
66		ax-17 1317	. . . . . . . . . . . . . . 15 |- (z = C -> A.w z = C)
67	44	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (y = w -> (z = C <-> z = [_w / y]_C))
68	66, 64, 67	cbvrex 2279	. . . . . . . . . . . . . 14 |- (E.y e. B z = C <-> E.w e. B z = [_w / y]_C)
69	68	anbi2i 538	. . . . . . . . . . . . 13 |- ((E.y e. B x = C /\ E.y e. B z = C) <-> (E.y e. B x = C /\ E.w e. B z = [_w / y]_C))
70	65, 69	bitr4i 193	. . . . . . . . . . . 12 |- (E.y e. B E.w e. B (x = C /\ z = [_w / y]_C) <-> (E.y e. B x = C /\ E.y e. B z = C))
71	60, 70	syl5ibr 224	. . . . . . . . . . 11 |- (E!x e. A A.y e. B x = C -> ((E.y e. B x = C /\ E.y e. B z = C) -> x = z))
72	71	a1d 15	. . . . . . . . . 10 |- (E!x e. A A.y e. B x = C -> (z e. A -> ((E.y e. B x = C /\ E.y e. B z = C) -> x = z)))
73	72	r19.21aiv 2175	. . . . . . . . 9 |- (E!x e. A A.y e. B x = C -> A.z e. A ((E.y e. B x = C /\ E.y e. B z = C) -> x = z))
74	73	a1d 15	. . . . . . . 8 |- (E!x e. A A.y e. B x = C -> (x e. A -> A.z e. A ((E.y e. B x = C /\ E.y e. B z = C) -> x = z)))
75	25, 74	r19.21ai 2174	. . . . . . 7 |- (E!x e. A A.y e. B x = C -> A.x e. A A.z e. A ((E.y e. B x = C /\ E.y e. B z = C) -> x = z))
76	75	adantl 424	. . . . . 6 |- ((B =/= (/) /\ E!x e. A A.y e. B x = C) -> A.x e. A A.z e. A ((E.y e. B x = C /\ E.y e. B z = C) -> x = z))
77	17, 24, 76	sylanbrc 527	. . . . 5 |- ((B =/= (/) /\ E!x e. A A.y e. B x = C) -> E!x e. A E.y e. B x = C)
78	77	ex 402	. . . 4 |- (B =/= (/) -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))
79	78	a1d 15	. . 3 |- (B =/= (/) -> (U.A =/= |^|A -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C)))
80	14, 79	pm2.61ine 2089	. 2 |- (U.A =/= |^|A -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))
81	80, 78	jaoi 368	1 |- ((U.A =/= |^|A \/ B =/= (/)) -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771   =/= wne 2017  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  [_csb 2540  (/)c0 2875  {csn 3044  U.cuni 3177  |^|cint 3214

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-uni 3178  df-int 3215

Copyright terms: Public domain