Theorem eueq3 3011

Description: Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.)

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 groups:   ph,x   ps,x   x,A   x,B   x,C

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		eueq3.1	. . . 4 |- A e. _V
2	1	eueq1 3009	. . 3 |- E!x x = A
3		ibar 490	. . . . . 6 |- (ph -> (x = A <-> (ph /\ x = A)))
4		pm2.45 386	. . . . . . . . . 10 |- (-. (ph \/ ps) -> -. ph)
5		eueq3.4	. . . . . . . . . . . 12 |- -. (ph /\ ps)
6	5	imnani 412	. . . . . . . . . . 11 |- (ph -> -. ps)
7	6	con2i 112	. . . . . . . . . 10 |- (ps -> -. ph)
8	4, 7	jaoi 368	. . . . . . . . 9 |- ((-. (ph \/ ps) \/ ps) -> -. ph)
9	8	con2i 112	. . . . . . . 8 |- (ph -> -. (-. (ph \/ ps) \/ ps))
10	4	con2i 112	. . . . . . . . . 10 |- (ph -> -. -. (ph \/ ps))
11	10	bianfd 892	. . . . . . . . 9 |- (ph -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
12	6	bianfd 892	. . . . . . . . 9 |- (ph -> (ps <-> (ps /\ x = C)))
13	11, 12	orbi12d 690	. . . . . . . 8 |- (ph -> ((-. (ph \/ ps) \/ ps) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
14	9, 13	mtbid 291	. . . . . . 7 |- (ph -> -. ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
15		biorf 394	. . . . . . 7 |- (-. ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) -> ((ph /\ x = A) <-> (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) \/ (ph /\ x = A))))
16	14, 15	syl 15	. . . . . 6 |- (ph -> ((ph /\ x = A) <-> (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) \/ (ph /\ x = A))))
17	3, 16	bitrd 244	. . . . 5 |- (ph -> (x = A <-> (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) \/ (ph /\ x = A))))
18		3orrot 940	. . . . . 6 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C) \/ (ph /\ x = A)))
19		df-3or 935	. . . . . 6 |- (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C) \/ (ph /\ x = A)) <-> (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) \/ (ph /\ x = A)))
20	18, 19	bitri 240	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> (((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) \/ (ph /\ x = A)))
21	17, 20	syl6bbr 254	. . . 4 |- (ph -> (x = A <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
22	21	eubidv 2212	. . 3 |- (ph -> (E!x x = A <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
23	2, 22	mpbii 202	. 2 |- (ph -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
24		eueq3.3	. . . 4 |- C e. _V
25	24	eueq1 3009	. . 3 |- E!x x = C
26		ibar 490	. . . . . 6 |- (ps -> (x = C <-> (ps /\ x = C)))
27	6	adantr 451	. . . . . . . . 9 |- ((ph /\ x = A) -> -. ps)
28		pm2.46 387	. . . . . . . . . 10 |- (-. (ph \/ ps) -> -. ps)
29	28	adantr 451	. . . . . . . . 9 |- ((-. (ph \/ ps) /\ x = B) -> -. ps)
30	27, 29	jaoi 368	. . . . . . . 8 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) -> -. ps)
31	30	con2i 112	. . . . . . 7 |- (ps -> -. ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)))
32		biorf 394	. . . . . . 7 |- (-. ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) -> ((ps /\ x = C) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
33	31, 32	syl 15	. . . . . 6 |- (ps -> ((ps /\ x = C) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
34	26, 33	bitrd 244	. . . . 5 |- (ps -> (x = C <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
35		df-3or 935	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C)))
36	34, 35	syl6bbr 254	. . . 4 |- (ps -> (x = C <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
37	36	eubidv 2212	. . 3 |- (ps -> (E!x x = C <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
38	25, 37	mpbii 202	. 2 |- (ps -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
39		eueq3.2	. . . 4 |- B e. _V
40	39	eueq1 3009	. . 3 |- E!x x = B
41		ibar 490	. . . . . 6 |- (-. (ph \/ ps) -> (x = B <-> (-. (ph \/ ps) /\ x = B)))
42		simpl 443	. . . . . . . . 9 |- ((ph /\ x = A) -> ph)
43		simpl 443	. . . . . . . . 9 |- ((ps /\ x = C) -> ps)
44	42, 43	orim12i 502	. . . . . . . 8 |- (((ph /\ x = A) \/ (ps /\ x = C)) -> (ph \/ ps))
45	44	con3i 127	. . . . . . 7 |- (-. (ph \/ ps) -> -. ((ph /\ x = A) \/ (ps /\ x = C)))
46		biorf 394	. . . . . . 7 |- (-. ((ph /\ x = A) \/ (ps /\ x = C)) -> ((-. (ph \/ ps) /\ x = B) <-> (((ph /\ x = A) \/ (ps /\ x = C)) \/ (-. (ph \/ ps) /\ x = B))))
47	45, 46	syl 15	. . . . . 6 |- (-. (ph \/ ps) -> ((-. (ph \/ ps) /\ x = B) <-> (((ph /\ x = A) \/ (ps /\ x = C)) \/ (-. (ph \/ ps) /\ x = B))))
48	41, 47	bitrd 244	. . . . 5 |- (-. (ph \/ ps) -> (x = B <-> (((ph /\ x = A) \/ (ps /\ x = C)) \/ (-. (ph \/ ps) /\ x = B))))
49		3orcomb 944	. . . . . 6 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ (ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B)))
50		df-3or 935	. . . . . 6 |- (((ph /\ x = A) \/ (ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B)) <-> (((ph /\ x = A) \/ (ps /\ x = C)) \/ (-. (ph \/ ps) /\ x = B)))
51	49, 50	bitri 240	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (ps /\ x = C)) \/ (-. (ph \/ ps) /\ x = B)))
52	48, 51	syl6bbr 254	. . . 4 |- (-. (ph \/ ps) -> (x = B <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
53	52	eubidv 2212	. . 3 |- (-. (ph \/ ps) -> (E!x x = B <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
54	40, 53	mpbii 202	. 2 |- (-. (ph \/ ps) -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
55	23, 38, 54	ecase3 907	1 |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Syntax hints:  -. wn 3   <-> wb 176   \/ wo 357   /\ wa 358   \/ w3o 933   = wceq 1642   e. wcel 1710  E!weu 2204  _Vcvv 2859

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-3or 935  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-v 2861

This theorem is referenced by:  moeq3  3013