Theorem eueq3 1430

Description: Equality has existential uniqueness (split into 3 cases).

Hypotheses

Ref	Expression
eueq3.1	|- A e. V
eueq3.2	|- B e. V
eueq3.3	|- C e. V
eueq3.4	|- -. (ph /\ ps)

Assertion

Ref	Expression
eueq3	|- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Distinct variable group(s):   ph,x   ps,x   x,A   x,B   x,C

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		euorv 1025	. . . 4 |- ((-. (-. (ph \/ ps) \/ ps) /\ E!x(ph /\ x = A)) -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
2		pm2.45 228	. . . . . 6 |- (-. (ph \/ ps) -> -. ph)
3		eueq3.4	. . . . . . . 8 |- -. (ph /\ ps)
4		imnan 207	. . . . . . . 8 |- ((ph -> -. ps) <-> -. (ph /\ ps))
5	3, 4	mpbir 165	. . . . . . 7 |- (ph -> -. ps)
6	5	con2i 89	. . . . . 6 |- (ps -> -. ph)
7	2, 6	jaoi 275	. . . . 5 |- ((-. (ph \/ ps) \/ ps) -> -. ph)
8	7	con2i 89	. . . 4 |- (ph -> -. (-. (ph \/ ps) \/ ps))
9		eueq3.1	. . . . . 6 |- A e. V
10	9	eueq1 1428	. . . . 5 |- E!x x = A
11		euanv 1053	. . . . . 6 |- (E!x(ph /\ x = A) <-> (ph /\ E!x x = A))
12	11	biimpr 134	. . . . 5 |- ((ph /\ E!x x = A) -> E!x(ph /\ x = A))
13	10, 12	mpan2 519	. . . 4 |- (ph -> E!x(ph /\ x = A))
14	1, 8, 13	sylanc 361	. . 3 |- (ph -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
15		negb 79	. . . . . . . . 9 |- ((ph \/ ps) -> -. -. (ph \/ ps))
16	15	orci 226	. . . . . . . 8 |- (ph -> -. -. (ph \/ ps))
17	16	bianfd 554	. . . . . . 7 |- (ph -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
18	5	bianfd 554	. . . . . . 7 |- (ph -> (ps <-> (ps /\ x = C)))
19	17, 18	orbi12d 475	. . . . . 6 |- (ph -> ((-. (ph \/ ps) \/ ps) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
20	19	orbi2d 466	. . . . 5 |- (ph -> (((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
21		orcom 209	. . . . 5 |- (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)))
22		3orass 584	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
23	20, 21, 22	3bitr4g 428	. . . 4 |- (ph -> (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
24	23	bieudv 1013	. . 3 |- (ph -> (E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
25	14, 24	mpbid 170	. 2 |- (ph -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
26		euorv 1025	. . . 4 |- ((-. (ph \/ -. (ph \/ ps)) /\ E!x(ps /\ x = C)) -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
27		pm2.46 229	. . . . . 6 |- (-. (ph \/ ps) -> -. ps)
28	5, 27	jaoi 275	. . . . 5 |- ((ph \/ -. (ph \/ ps)) -> -. ps)
29	28	con2i 89	. . . 4 |- (ps -> -. (ph \/ -. (ph \/ ps)))
30		eueq3.3	. . . . . 6 |- C e. V
31	30	eueq1 1428	. . . . 5 |- E!x x = C
32		euanv 1053	. . . . . 6 |- (E!x(ps /\ x = C) <-> (ps /\ E!x x = C))
33	32	biimpr 134	. . . . 5 |- ((ps /\ E!x x = C) -> E!x(ps /\ x = C))
34	31, 33	mpan2 519	. . . 4 |- (ps -> E!x(ps /\ x = C))
35	26, 29, 34	sylanc 361	. . 3 |- (ps -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
36	6	bianfd 554	. . . . . . 7 |- (ps -> (ph <-> (ph /\ x = A)))
37	15	olci 227	. . . . . . . 8 |- (ps -> -. -. (ph \/ ps))
38	37	bianfd 554	. . . . . . 7 |- (ps -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
39	36, 38	orbi12d 475	. . . . . 6 |- (ps -> ((ph \/ -. (ph \/ ps)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B))))
40	39	orbi1d 467	. . . . 5 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
41		df-3or 582	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C)))
42	40, 41	syl6bbr 416	. . . 4 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
43	42	bieudv 1013	. . 3 |- (ps -> (E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
44	35, 43	mpbid 170	. 2 |- (ps -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
45		eueq3.2	. . . . . 6 |- B e. V
46	45	eueq1 1428	. . . . 5 |- E!x x = B
47		euanv 1053	. . . . . 6 |- (E!x(-. (ph \/ ps) /\ x = B) <-> (-. (ph \/ ps) /\ E!x x = B))
48	47	biimpr 134	. . . . 5 |- ((-. (ph \/ ps) /\ E!x x = B) -> E!x(-. (ph \/ ps) /\ x = B))
49	46, 48	mpan2 519	. . . 4 |- (-. (ph \/ ps) -> E!x(-. (ph \/ ps) /\ x = B))
50		euorv 1025	. . . 4 |- ((-. (ph \/ ps) /\ E!x(-. (ph \/ ps) /\ x = B)) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
51	49, 50	mpdan 527	. . 3 |- (-. (ph \/ ps) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
52	2	bianfd 554	. . . . . 6 |- (-. (ph \/ ps) -> (ph <-> (ph /\ x = A)))
53	27	bianfd 554	. . . . . . . 8 |- (-. (ph \/ ps) -> (ps <-> (ps /\ x = C)))
54	53	orbi1d 467	. . . . . . 7 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B))))
55		orcom 209	. . . . . . 7 |- (((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
56	54, 55	syl6bb 414	. . . . . 6 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
57	52, 56	orbi12d 475	. . . . 5 |- (-. (ph \/ ps) -> ((ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
58		orass 218	. . . . 5 |- (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> (ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))))
59	57, 58, 22	3bitr4g 428	. . . 4 |- (-. (ph \/ ps) -> (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
60	59	bieudv 1013	. . 3 |- (-. (ph \/ ps) -> (E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
61	51, 60	mpbid 170	. 2 |- (-. (ph \/ ps) -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
62	25, 44, 61	ecase3 559	1 |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195   /\ wa 196   \/ w3o 580  E!weu 1007   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  moeq3 1432

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org