Theorem reuind 2450

Description: Existential uniqueness via an indirect equality.

Hypotheses

Ref	Expression
reuind.1	|- (x = y -> (ph <-> ps))
reuind.2	|- (x = y -> A = B)

Assertion

Ref	Expression
reuind	|- ((A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) /\ E.x(A e. C /\ ph)) -> E!z e. C A.x((A e. C /\ ph) -> z = A))

Distinct variable groups:   y,z,A   x,z,B   x,y,C,z   ph,y,z   ps,x,z

Proof of Theorem reuind

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . . . 5 |- (z = w -> (z = A <-> w = A))
2	1	imbi2d 674	. . . 4 |- (z = w -> (((A e. C /\ ph) -> z = A) <-> ((A e. C /\ ph) -> w = A)))
3	2	albidv 1656	. . 3 |- (z = w -> (A.x((A e. C /\ ph) -> z = A) <-> A.x((A e. C /\ ph) -> w = A)))
4	3	reu4 2446	. 2 |- (E!z e. C A.x((A e. C /\ ph) -> z = A) <-> (E.z e. C A.x((A e. C /\ ph) -> z = A) /\ A.z e. C A.w e. C ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> z = w)))
5		eqeq2 1893	. . . . . . . . . 10 |- (A = B -> (z = A <-> z = B))
6	5	imim2i 11	. . . . . . . . 9 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> (((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = A <-> z = B)))
7		bi2 166	. . . . . . . . . . 11 |- ((z = A <-> z = B) -> (z = B -> z = A))
8	7	imim2i 11	. . . . . . . . . 10 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = A <-> z = B)) -> (((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = B -> z = A)))
9		an23 543	. . . . . . . . . . . . 13 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) /\ z = B) <-> (((A e. C /\ ph) /\ z = B) /\ (B e. C /\ ps)))
10		ancom 482	. . . . . . . . . . . . . 14 |- (((A e. C /\ ph) /\ z = B) <-> (z = B /\ (A e. C /\ ph)))
11	10	anbi1i 539	. . . . . . . . . . . . 13 |- ((((A e. C /\ ph) /\ z = B) /\ (B e. C /\ ps)) <-> ((z = B /\ (A e. C /\ ph)) /\ (B e. C /\ ps)))
12		an23 543	. . . . . . . . . . . . 13 |- (((z = B /\ (A e. C /\ ph)) /\ (B e. C /\ ps)) <-> ((z = B /\ (B e. C /\ ps)) /\ (A e. C /\ ph)))
13	9, 11, 12	3bitri 194	. . . . . . . . . . . 12 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) /\ z = B) <-> ((z = B /\ (B e. C /\ ps)) /\ (A e. C /\ ph)))
14	13	imbi1i 203	. . . . . . . . . . 11 |- (((((A e. C /\ ph) /\ (B e. C /\ ps)) /\ z = B) -> z = A) <-> (((z = B /\ (B e. C /\ ps)) /\ (A e. C /\ ph)) -> z = A))
15		impexp 374	. . . . . . . . . . 11 |- (((((A e. C /\ ph) /\ (B e. C /\ ps)) /\ z = B) -> z = A) <-> (((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = B -> z = A)))
16		impexp 374	. . . . . . . . . . 11 |- ((((z = B /\ (B e. C /\ ps)) /\ (A e. C /\ ph)) -> z = A) <-> ((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
17	14, 15, 16	3bitr3i 198	. . . . . . . . . 10 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = B -> z = A)) <-> ((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
18	8, 17	sylib 215	. . . . . . . . 9 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = A <-> z = B)) -> ((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
19	6, 18	syl 12	. . . . . . . 8 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> ((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
20	19	2alimi 1339	. . . . . . 7 |- (A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> A.xA.y((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
21		19.23v 1672	. . . . . . . . . 10 |- (A.y((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> (E.y(z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
22		an12 542	. . . . . . . . . . . . . 14 |- ((z = B /\ (B e. C /\ ps)) <-> (B e. C /\ (z = B /\ ps)))
23		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (z = B -> (z e. C <-> B e. C))
24	23	adantr 425	. . . . . . . . . . . . . . 15 |- ((z = B /\ ps) -> (z e. C <-> B e. C))
25	24	pm5.32ri 708	. . . . . . . . . . . . . 14 |- ((z e. C /\ (z = B /\ ps)) <-> (B e. C /\ (z = B /\ ps)))
26	22, 25	bitr4i 193	. . . . . . . . . . . . 13 |- ((z = B /\ (B e. C /\ ps)) <-> (z e. C /\ (z = B /\ ps)))
27	26	exbii 1398	. . . . . . . . . . . 12 |- (E.y(z = B /\ (B e. C /\ ps)) <-> E.y(z e. C /\ (z = B /\ ps)))
28		19.42v 1688	. . . . . . . . . . . 12 |- (E.y(z e. C /\ (z = B /\ ps)) <-> (z e. C /\ E.y(z = B /\ ps)))
29	27, 28	bitri 190	. . . . . . . . . . 11 |- (E.y(z = B /\ (B e. C /\ ps)) <-> (z e. C /\ E.y(z = B /\ ps)))
30	29	imbi1i 203	. . . . . . . . . 10 |- ((E.y(z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> ((z e. C /\ E.y(z = B /\ ps)) -> ((A e. C /\ ph) -> z = A)))
31	21, 30	bitri 190	. . . . . . . . 9 |- (A.y((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> ((z e. C /\ E.y(z = B /\ ps)) -> ((A e. C /\ ph) -> z = A)))
32	31	albii 1346	. . . . . . . 8 |- (A.xA.y((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> A.x((z e. C /\ E.y(z = B /\ ps)) -> ((A e. C /\ ph) -> z = A)))
33		19.21v 1663	. . . . . . . 8 |- (A.x((z e. C /\ E.y(z = B /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> ((z e. C /\ E.y(z = B /\ ps)) -> A.x((A e. C /\ ph) -> z = A)))
34	32, 33	bitri 190	. . . . . . 7 |- (A.xA.y((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)) <-> ((z e. C /\ E.y(z = B /\ ps)) -> A.x((A e. C /\ ph) -> z = A)))
35	20, 34	sylib 215	. . . . . 6 |- (A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> ((z e. C /\ E.y(z = B /\ ps)) -> A.x((A e. C /\ ph) -> z = A)))
36	35	exp3a 405	. . . . 5 |- (A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> (z e. C -> (E.y(z = B /\ ps) -> A.x((A e. C /\ ph) -> z = A))))
37	36	reximdvai 2201	. . . 4 |- (A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> (E.z e. C E.y(z = B /\ ps) -> E.z e. C A.x((A e. C /\ ph) -> z = A)))
38		reuind.2	. . . . . . . 8 |- (x = y -> A = B)
39	38	eleq1d 1963	. . . . . . 7 |- (x = y -> (A e. C <-> B e. C))
40		reuind.1	. . . . . . 7 |- (x = y -> (ph <-> ps))
41	39, 40	anbi12d 690	. . . . . 6 |- (x = y -> ((A e. C /\ ph) <-> (B e. C /\ ps)))
42	41	cbvexv 1697	. . . . 5 |- (E.x(A e. C /\ ph) <-> E.y(B e. C /\ ps))
43		risset 2145	. . . . . . 7 |- (B e. C <-> E.z e. C z = B)
44	43	anbi1i 539	. . . . . 6 |- ((B e. C /\ ps) <-> (E.z e. C z = B /\ ps))
45	44	exbii 1398	. . . . 5 |- (E.y(B e. C /\ ps) <-> E.y(E.z e. C z = B /\ ps))
46		rexcom4 2312	. . . . . 6 |- (E.z e. C E.y(z = B /\ ps) <-> E.yE.z e. C (z = B /\ ps))
47		r19.41v 2236	. . . . . . 7 |- (E.z e. C (z = B /\ ps) <-> (E.z e. C z = B /\ ps))
48	47	exbii 1398	. . . . . 6 |- (E.yE.z e. C (z = B /\ ps) <-> E.y(E.z e. C z = B /\ ps))
49	46, 48	bitr2i 191	. . . . 5 |- (E.y(E.z e. C z = B /\ ps) <-> E.z e. C E.y(z = B /\ ps))
50	42, 45, 49	3bitri 194	. . . 4 |- (E.x(A e. C /\ ph) <-> E.z e. C E.y(z = B /\ ps))
51	37, 50	syl5ib 223	. . 3 |- (A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> (E.x(A e. C /\ ph) -> E.z e. C A.x((A e. C /\ ph) -> z = A)))
52	51	imp 377	. 2 |- ((A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) /\ E.x(A e. C /\ ph)) -> E.z e. C A.x((A e. C /\ ph) -> z = A))
53		19.23v 1672	. . . . . . . 8 |- (A.x((A e. C /\ ph) -> z = w) <-> (E.x(A e. C /\ ph) -> z = w))
54	53	biimpi 168	. . . . . . 7 |- (A.x((A e. C /\ ph) -> z = w) -> (E.x(A e. C /\ ph) -> z = w))
55	54	com12 14	. . . . . 6 |- (E.x(A e. C /\ ph) -> (A.x((A e. C /\ ph) -> z = w) -> z = w))
56		19.26 1416	. . . . . . 7 |- (A.x(((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) <-> (A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)))
57		prth 615	. . . . . . . . 9 |- ((((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) -> (((A e. C /\ ph) /\ (A e. C /\ ph)) -> (z = A /\ w = A)))
58		pm4.24 479	. . . . . . . . . . 11 |- ((A e. C /\ ph) <-> ((A e. C /\ ph) /\ (A e. C /\ ph)))
59	58	biimpi 168	. . . . . . . . . 10 |- ((A e. C /\ ph) -> ((A e. C /\ ph) /\ (A e. C /\ ph)))
60		eqtr3 1907	. . . . . . . . . 10 |- ((z = A /\ w = A) -> z = w)
61	59, 60	imim12i 21	. . . . . . . . 9 |- ((((A e. C /\ ph) /\ (A e. C /\ ph)) -> (z = A /\ w = A)) -> ((A e. C /\ ph) -> z = w))
62	57, 61	syl 12	. . . . . . . 8 |- ((((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) -> ((A e. C /\ ph) -> z = w))
63	62	alimi 1338	. . . . . . 7 |- (A.x(((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) -> A.x((A e. C /\ ph) -> z = w))
64	56, 63	sylbir 218	. . . . . 6 |- ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> A.x((A e. C /\ ph) -> z = w))
65	55, 64	syl5 20	. . . . 5 |- (E.x(A e. C /\ ph) -> ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> z = w))
66	65	a1d 15	. . . 4 |- (E.x(A e. C /\ ph) -> ((z e. C /\ w e. C) -> ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> z = w)))
67	66	r19.21aivv 2183	. . 3 |- (E.x(A e. C /\ ph) -> A.z e. C A.w e. C ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> z = w))
68	67	adantl 424	. 2 |- ((A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) /\ E.x(A e. C /\ ph)) -> A.z e. C A.w e. C ((A.x((A e. C /\ ph) -> z = A) /\ A.x((A e. C /\ ph) -> w = A)) -> z = w))
69	4, 52, 68	sylanbrc 527	1 |- ((A.xA.y(((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) /\ E.x(A e. C /\ ph)) -> E!z e. C A.x((A e. C /\ ph) -> z = A))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  E!wreu 2107

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-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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-reu 2111  df-v 2294

Copyright terms: Public domain