Theorem reuind 3040

Description: Existential uniqueness via an indirect equality. (Contributed by NM, 16-Oct-2010.)

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

Allowed substitution hints:   ph(x)   ps(y)   A(x)   B(y)

Proof of Theorem reuind

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reuind.2	. . . . . . . 8 |- (x = y -> A = B)
2	1	eleq1d 2419	. . . . . . 7 |- (x = y -> (A e. C <-> B e. C))
3		reuind.1	. . . . . . 7 |- (x = y -> (ph <-> ps))
4	2, 3	anbi12d 691	. . . . . 6 |- (x = y -> ((A e. C /\ ph) <-> (B e. C /\ ps)))
5	4	cbvexv 2003	. . . . 5 |- (E.x(A e. C /\ ph) <-> E.y(B e. C /\ ps))
6		r19.41v 2765	. . . . . . 7 |- (E.z e. C (z = B /\ ps) <-> (E.z e. C z = B /\ ps))
7	6	exbii 1582	. . . . . 6 |- (E.yE.z e. C (z = B /\ ps) <-> E.y(E.z e. C z = B /\ ps))
8		rexcom4 2879	. . . . . 6 |- (E.z e. C E.y(z = B /\ ps) <-> E.yE.z e. C (z = B /\ ps))
9		risset 2662	. . . . . . . 8 |- (B e. C <-> E.z e. C z = B)
10	9	anbi1i 676	. . . . . . 7 |- ((B e. C /\ ps) <-> (E.z e. C z = B /\ ps))
11	10	exbii 1582	. . . . . 6 |- (E.y(B e. C /\ ps) <-> E.y(E.z e. C z = B /\ ps))
12	7, 8, 11	3bitr4ri 269	. . . . 5 |- (E.y(B e. C /\ ps) <-> E.z e. C E.y(z = B /\ ps))
13	5, 12	bitri 240	. . . 4 |- (E.x(A e. C /\ ph) <-> E.z e. C E.y(z = B /\ ps))
14		eqeq2 2362	. . . . . . . . . 10 |- (A = B -> (z = A <-> z = B))
15	14	imim2i 13	. . . . . . . . 9 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> (((A e. C /\ ph) /\ (B e. C /\ ps)) -> (z = A <-> z = B)))
16		bi2 189	. . . . . . . . . . 11 |- ((z = A <-> z = B) -> (z = B -> z = A))
17	16	imim2i 13	. . . . . . . . . 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)))
18		an31 775	. . . . . . . . . . . 12 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) /\ z = B) <-> ((z = B /\ (B e. C /\ ps)) /\ (A e. C /\ ph)))
19	18	imbi1i 315	. . . . . . . . . . 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))
20		impexp 433	. . . . . . . . . . 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)))
21		impexp 433	. . . . . . . . . . 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)))
22	19, 20, 21	3bitr3i 266	. . . . . . . . . 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)))
23	17, 22	sylib 188	. . . . . . . . 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)))
24	15, 23	syl 15	. . . . . . . 8 |- ((((A e. C /\ ph) /\ (B e. C /\ ps)) -> A = B) -> ((z = B /\ (B e. C /\ ps)) -> ((A e. C /\ ph) -> z = A)))
25	24	2alimi 1560	. . . . . . 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)))
26		19.23v 1891	. . . . . . . . . 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)))
27		an12 772	. . . . . . . . . . . . . 14 |- ((z = B /\ (B e. C /\ ps)) <-> (B e. C /\ (z = B /\ ps)))
28		eleq1 2413	. . . . . . . . . . . . . . . 16 |- (z = B -> (z e. C <-> B e. C))
29	28	adantr 451	. . . . . . . . . . . . . . 15 |- ((z = B /\ ps) -> (z e. C <-> B e. C))
30	29	pm5.32ri 619	. . . . . . . . . . . . . 14 |- ((z e. C /\ (z = B /\ ps)) <-> (B e. C /\ (z = B /\ ps)))
31	27, 30	bitr4i 243	. . . . . . . . . . . . 13 |- ((z = B /\ (B e. C /\ ps)) <-> (z e. C /\ (z = B /\ ps)))
32	31	exbii 1582	. . . . . . . . . . . 12 |- (E.y(z = B /\ (B e. C /\ ps)) <-> E.y(z e. C /\ (z = B /\ ps)))
33		19.42v 1905	. . . . . . . . . . . 12 |- (E.y(z e. C /\ (z = B /\ ps)) <-> (z e. C /\ E.y(z = B /\ ps)))
34	32, 33	bitri 240	. . . . . . . . . . 11 |- (E.y(z = B /\ (B e. C /\ ps)) <-> (z e. C /\ E.y(z = B /\ ps)))
35	34	imbi1i 315	. . . . . . . . . 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)))
36	26, 35	bitri 240	. . . . . . . . 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)))
37	36	albii 1566	. . . . . . . 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)))
38		19.21v 1890	. . . . . . . 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)))
39	37, 38	bitri 240	. . . . . . 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)))
40	25, 39	sylib 188	. . . . . 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)))
41	40	exp3a 425	. . . . 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))))
42	41	reximdvai 2725	. . . 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)))
43	13, 42	syl5bi 208	. . 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)))
44	43	imp 418	. 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))
45		pm4.24 624	. . . . . . . . 9 |- ((A e. C /\ ph) <-> ((A e. C /\ ph) /\ (A e. C /\ ph)))
46	45	biimpi 186	. . . . . . . 8 |- ((A e. C /\ ph) -> ((A e. C /\ ph) /\ (A e. C /\ ph)))
47		prth 554	. . . . . . . 8 |- ((((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) -> (((A e. C /\ ph) /\ (A e. C /\ ph)) -> (z = A /\ w = A)))
48		eqtr3 2372	. . . . . . . 8 |- ((z = A /\ w = A) -> z = w)
49	46, 47, 48	syl56 30	. . . . . . 7 |- ((((A e. C /\ ph) -> z = A) /\ ((A e. C /\ ph) -> w = A)) -> ((A e. C /\ ph) -> z = w))
50	49	alanimi 1562	. . . . . 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))
51		19.23v 1891	. . . . . . . 8 |- (A.x((A e. C /\ ph) -> z = w) <-> (E.x(A e. C /\ ph) -> z = w))
52	51	biimpi 186	. . . . . . 7 |- (A.x((A e. C /\ ph) -> z = w) -> (E.x(A e. C /\ ph) -> z = w))
53	52	com12 27	. . . . . 6 |- (E.x(A e. C /\ ph) -> (A.x((A e. C /\ ph) -> z = w) -> z = w))
54	50, 53	syl5 28	. . . . 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))
55	54	a1d 22	. . . 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)))
56	55	ralrimivv 2706	. . 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))
57	56	adantl 452	. 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))
58		eqeq1 2359	. . . . 5 |- (z = w -> (z = A <-> w = A))
59	58	imbi2d 307	. . . 4 |- (z = w -> (((A e. C /\ ph) -> z = A) <-> ((A e. C /\ ph) -> w = A)))
60	59	albidv 1625	. . 3 |- (z = w -> (A.x((A e. C /\ ph) -> z = A) <-> A.x((A e. C /\ ph) -> w = A)))
61	60	reu4 3031	. 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)))
62	44, 57, 61	sylanbrc 645	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 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  A.wral 2615  E.wrex 2616  E!wreu 2617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-v 2862

This theorem is referenced by: (None)