Theorem euind 2439

Description: Existential uniqueness via an indirect equality.

Hypotheses

Ref	Expression
euind.0	|- B e. _V
euind.1	|- (x = y -> (ph <-> ps))
euind.2	|- (x = y -> A = B)

Assertion

Ref	Expression
euind	|- ((A.xA.y((ph /\ ps) -> A = B) /\ E.xph) -> E!zA.x(ph -> z = A))

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

Proof of Theorem euind

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . . . 5 |- (z = w -> (z = A <-> w = A))
2	1	imbi2d 674	. . . 4 |- (z = w -> ((ph -> z = A) <-> (ph -> w = A)))
3	2	albidv 1656	. . 3 |- (z = w -> (A.x(ph -> z = A) <-> A.x(ph -> w = A)))
4	3	eu4 1806	. 2 |- (E!zA.x(ph -> z = A) <-> (E.zA.x(ph -> z = A) /\ A.zA.w((A.x(ph -> z = A) /\ A.x(ph -> w = A)) -> z = w)))
5		eqeq2 1893	. . . . . . . . 9 |- (A = B -> (z = A <-> z = B))
6	5	imim2i 11	. . . . . . . 8 |- (((ph /\ ps) -> A = B) -> ((ph /\ ps) -> (z = A <-> z = B)))
7		bi2 166	. . . . . . . . . 10 |- ((z = A <-> z = B) -> (z = B -> z = A))
8	7	imim2i 11	. . . . . . . . 9 |- (((ph /\ ps) -> (z = A <-> z = B)) -> ((ph /\ ps) -> (z = B -> z = A)))
9		an23 543	. . . . . . . . . . . 12 |- (((ph /\ ps) /\ z = B) <-> ((ph /\ z = B) /\ ps))
10		ancom 482	. . . . . . . . . . . . 13 |- ((ph /\ z = B) <-> (z = B /\ ph))
11	10	anbi1i 539	. . . . . . . . . . . 12 |- (((ph /\ z = B) /\ ps) <-> ((z = B /\ ph) /\ ps))
12		an23 543	. . . . . . . . . . . 12 |- (((z = B /\ ph) /\ ps) <-> ((z = B /\ ps) /\ ph))
13	9, 11, 12	3bitri 194	. . . . . . . . . . 11 |- (((ph /\ ps) /\ z = B) <-> ((z = B /\ ps) /\ ph))
14	13	imbi1i 203	. . . . . . . . . 10 |- ((((ph /\ ps) /\ z = B) -> z = A) <-> (((z = B /\ ps) /\ ph) -> z = A))
15		impexp 374	. . . . . . . . . 10 |- ((((ph /\ ps) /\ z = B) -> z = A) <-> ((ph /\ ps) -> (z = B -> z = A)))
16		impexp 374	. . . . . . . . . 10 |- ((((z = B /\ ps) /\ ph) -> z = A) <-> ((z = B /\ ps) -> (ph -> z = A)))
17	14, 15, 16	3bitr3i 198	. . . . . . . . 9 |- (((ph /\ ps) -> (z = B -> z = A)) <-> ((z = B /\ ps) -> (ph -> z = A)))
18	8, 17	sylib 215	. . . . . . . 8 |- (((ph /\ ps) -> (z = A <-> z = B)) -> ((z = B /\ ps) -> (ph -> z = A)))
19	6, 18	syl 12	. . . . . . 7 |- (((ph /\ ps) -> A = B) -> ((z = B /\ ps) -> (ph -> z = A)))
20	19	2alimi 1339	. . . . . 6 |- (A.xA.y((ph /\ ps) -> A = B) -> A.xA.y((z = B /\ ps) -> (ph -> z = A)))
21		19.23v 1672	. . . . . . . 8 |- (A.y((z = B /\ ps) -> (ph -> z = A)) <-> (E.y(z = B /\ ps) -> (ph -> z = A)))
22	21	albii 1346	. . . . . . 7 |- (A.xA.y((z = B /\ ps) -> (ph -> z = A)) <-> A.x(E.y(z = B /\ ps) -> (ph -> z = A)))
23		19.21v 1663	. . . . . . 7 |- (A.x(E.y(z = B /\ ps) -> (ph -> z = A)) <-> (E.y(z = B /\ ps) -> A.x(ph -> z = A)))
24	22, 23	bitri 190	. . . . . 6 |- (A.xA.y((z = B /\ ps) -> (ph -> z = A)) <-> (E.y(z = B /\ ps) -> A.x(ph -> z = A)))
25	20, 24	sylib 215	. . . . 5 |- (A.xA.y((ph /\ ps) -> A = B) -> (E.y(z = B /\ ps) -> A.x(ph -> z = A)))
26	25	eximdv 1669	. . . 4 |- (A.xA.y((ph /\ ps) -> A = B) -> (E.zE.y(z = B /\ ps) -> E.zA.x(ph -> z = A)))
27		euind.1	. . . . . 6 |- (x = y -> (ph <-> ps))
28	27	cbvexv 1697	. . . . 5 |- (E.xph <-> E.yps)
29		euind.0	. . . . . . . 8 |- B e. _V
30	29	isseti 2297	. . . . . . 7 |- E.z z = B
31	30	biantrur 794	. . . . . 6 |- (ps <-> (E.z z = B /\ ps))
32	31	exbii 1398	. . . . 5 |- (E.yps <-> E.y(E.z z = B /\ ps))
33		19.41v 1685	. . . . . . 7 |- (E.z(z = B /\ ps) <-> (E.z z = B /\ ps))
34	33	exbii 1398	. . . . . 6 |- (E.yE.z(z = B /\ ps) <-> E.y(E.z z = B /\ ps))
35		excom 1393	. . . . . 6 |- (E.yE.z(z = B /\ ps) <-> E.zE.y(z = B /\ ps))
36	34, 35	bitr3i 192	. . . . 5 |- (E.y(E.z z = B /\ ps) <-> E.zE.y(z = B /\ ps))
37	28, 32, 36	3bitri 194	. . . 4 |- (E.xph <-> E.zE.y(z = B /\ ps))
38	26, 37	syl5ib 223	. . 3 |- (A.xA.y((ph /\ ps) -> A = B) -> (E.xph -> E.zA.x(ph -> z = A)))
39	38	imp 377	. 2 |- ((A.xA.y((ph /\ ps) -> A = B) /\ E.xph) -> E.zA.x(ph -> z = A))
40		19.23v 1672	. . . . . . 7 |- (A.x(ph -> z = w) <-> (E.xph -> z = w))
41	40	biimpi 168	. . . . . 6 |- (A.x(ph -> z = w) -> (E.xph -> z = w))
42	41	com12 14	. . . . 5 |- (E.xph -> (A.x(ph -> z = w) -> z = w))
43		19.26 1416	. . . . . 6 |- (A.x((ph -> z = A) /\ (ph -> w = A)) <-> (A.x(ph -> z = A) /\ A.x(ph -> w = A)))
44		prth 615	. . . . . . . 8 |- (((ph -> z = A) /\ (ph -> w = A)) -> ((ph /\ ph) -> (z = A /\ w = A)))
45		pm4.24 479	. . . . . . . . . 10 |- (ph <-> (ph /\ ph))
46	45	biimpi 168	. . . . . . . . 9 |- (ph -> (ph /\ ph))
47		eqtr3 1907	. . . . . . . . 9 |- ((z = A /\ w = A) -> z = w)
48	46, 47	imim12i 21	. . . . . . . 8 |- (((ph /\ ph) -> (z = A /\ w = A)) -> (ph -> z = w))
49	44, 48	syl 12	. . . . . . 7 |- (((ph -> z = A) /\ (ph -> w = A)) -> (ph -> z = w))
50	49	alimi 1338	. . . . . 6 |- (A.x((ph -> z = A) /\ (ph -> w = A)) -> A.x(ph -> z = w))
51	43, 50	sylbir 218	. . . . 5 |- ((A.x(ph -> z = A) /\ A.x(ph -> w = A)) -> A.x(ph -> z = w))
52	42, 51	syl5 20	. . . 4 |- (E.xph -> ((A.x(ph -> z = A) /\ A.x(ph -> w = A)) -> z = w))
53	52	19.21aivv 1665	. . 3 |- (E.xph -> A.zA.w((A.x(ph -> z = A) /\ A.x(ph -> w = A)) -> z = w))
54	53	adantl 424	. 2 |- ((A.xA.y((ph /\ ps) -> A = B) /\ E.xph) -> A.zA.w((A.x(ph -> z = A) /\ A.x(ph -> w = A)) -> z = w))
55	4, 39, 54	sylanbrc 527	1 |- ((A.xA.y((ph /\ ps) -> A = B) /\ E.xph) -> E!zA.x(ph -> z = A))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  _Vcvv 2292

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

Copyright terms: Public domain