Theorem eueq3 3381

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 3379	. . 3 |- E! x x = A
3		ibar 525	. . . . . 6 |- ( ph -> ( x = A <-> ( ph /\ x = A ) ) )
4		pm2.45 412	. . . . . . . . . 10 |- ( -. ( ph \/ ps ) -> -. ph )
5		eueq3.4	. . . . . . . . . . . 12 |- -. ( ph /\ ps )
6	5	imnani 439	. . . . . . . . . . 11 |- ( ph -> -. ps )
7	6	con2i 134	. . . . . . . . . 10 |- ( ps -> -. ph )
8	4, 7	jaoi 394	. . . . . . . . 9 |- ( ( -. ( ph \/ ps ) \/ ps ) -> -. ph )
9	8	con2i 134	. . . . . . . 8 |- ( ph -> -. ( -. ( ph \/ ps ) \/ ps ) )
10	4	con2i 134	. . . . . . . . . 10 |- ( ph -> -. -. ( ph \/ ps ) )
11	10	bianfd 967	. . . . . . . . 9 |- ( ph -> ( -. ( ph \/ ps ) <-> ( -. ( ph \/ ps ) /\ x = B ) ) )
12	6	bianfd 967	. . . . . . . . 9 |- ( ph -> ( ps <-> ( ps /\ x = C ) ) )
13	11, 12	orbi12d 746	. . . . . . . 8 |- ( ph -> ( ( -. ( ph \/ ps ) \/ ps ) <-> ( ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
14	9, 13	mtbid 314	. . . . . . 7 |- ( ph -> -. ( ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) )
15		biorf 420	. . . . . . 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 17	. . . . . 6 |- ( ph -> ( ( ph /\ x = A ) <-> ( ( ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) \/ ( ph /\ x = A ) ) ) )
17	3, 16	bitrd 268	. . . . 5 |- ( ph -> ( x = A <-> ( ( ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) \/ ( ph /\ x = A ) ) ) )
18		3orrot 1044	. . . . . 6 |- ( ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) <-> ( ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) \/ ( ph /\ x = A ) ) )
19		df-3or 1038	. . . . . 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 264	. . . . 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 278	. . . 4 |- ( ph -> ( x = A <-> ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
22	21	eubidv 2490	. . 3 |- ( ph -> ( E! x x = A <-> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
23	2, 22	mpbii 223	. 2 |- ( ph -> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) )
24		eueq3.3	. . . 4 |- C e. _V
25	24	eueq1 3379	. . 3 |- E! x x = C
26		ibar 525	. . . . . 6 |- ( ps -> ( x = C <-> ( ps /\ x = C ) ) )
27	6	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x = A ) -> -. ps )
28		pm2.46 413	. . . . . . . . . 10 |- ( -. ( ph \/ ps ) -> -. ps )
29	28	adantr 481	. . . . . . . . 9 |- ( ( -. ( ph \/ ps ) /\ x = B ) -> -. ps )
30	27, 29	jaoi 394	. . . . . . . 8 |- ( ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) -> -. ps )
31	30	con2i 134	. . . . . . 7 |- ( ps -> -. ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) )
32		biorf 420	. . . . . . 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 17	. . . . . 6 |- ( ps -> ( ( ps /\ x = C ) <-> ( ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) \/ ( ps /\ x = C ) ) ) )
34	26, 33	bitrd 268	. . . . 5 |- ( ps -> ( x = C <-> ( ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) \/ ( ps /\ x = C ) ) ) )
35		df-3or 1038	. . . . 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 278	. . . 4 |- ( ps -> ( x = C <-> ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
37	36	eubidv 2490	. . 3 |- ( ps -> ( E! x x = C <-> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
38	25, 37	mpbii 223	. 2 |- ( ps -> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) )
39		eueq3.2	. . . 4 |- B e. _V
40	39	eueq1 3379	. . 3 |- E! x x = B
41		ibar 525	. . . . . 6 |- ( -. ( ph \/ ps ) -> ( x = B <-> ( -. ( ph \/ ps ) /\ x = B ) ) )
42		simpl 473	. . . . . . . . 9 |- ( ( ph /\ x = A ) -> ph )
43		simpl 473	. . . . . . . . 9 |- ( ( ps /\ x = C ) -> ps )
44	42, 43	orim12i 538	. . . . . . . 8 |- ( ( ( ph /\ x = A ) \/ ( ps /\ x = C ) ) -> ( ph \/ ps ) )
45	44	con3i 150	. . . . . . 7 |- ( -. ( ph \/ ps ) -> -. ( ( ph /\ x = A ) \/ ( ps /\ x = C ) ) )
46		biorf 420	. . . . . . 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 17	. . . . . 6 |- ( -. ( ph \/ ps ) -> ( ( -. ( ph \/ ps ) /\ x = B ) <-> ( ( ( ph /\ x = A ) \/ ( ps /\ x = C ) ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) ) )
48	41, 47	bitrd 268	. . . . 5 |- ( -. ( ph \/ ps ) -> ( x = B <-> ( ( ( ph /\ x = A ) \/ ( ps /\ x = C ) ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) ) )
49		3orcomb 1048	. . . . . 6 |- ( ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) <-> ( ( ph /\ x = A ) \/ ( ps /\ x = C ) \/ ( -. ( ph \/ ps ) /\ x = B ) ) )
50		df-3or 1038	. . . . . 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 264	. . . . 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 278	. . . 4 |- ( -. ( ph \/ ps ) -> ( x = B <-> ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
53	52	eubidv 2490	. . 3 |- ( -. ( ph \/ ps ) -> ( E! x x = B <-> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) ) )
54	40, 53	mpbii 223	. 2 |- ( -. ( ph \/ ps ) -> E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) ) )
55	23, 38, 54	ecase3 982	1 |- E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) )

Syntax hints:   -. wn 3   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   = wceq 1483   e. wcel 1990   E!weu 2470   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  moeq3  3383