Theorem eueq3 3613

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	⊢ 𝐴 ∈ V
eueq3.2	⊢ 𝐵 ∈ V
eueq3.3	⊢ 𝐶 ∈ V
eueq3.4	⊢ ¬ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
eueq3	⊢ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))

Distinct variable groups:   𝜑,𝑥   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		eueq3.1	. . . 4 ⊢ 𝐴 ∈ V
2	1	eueqi 3611	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐴
3		ibar 532	. . . . . 6 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (𝜑 ∧ 𝑥 = 𝐴)))
4		pm2.45 882	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
5		eueq3.4	. . . . . . . . . . . 12 ⊢ ¬ (𝜑 ∧ 𝜓)
6	5	imnani 404	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝜓)
7	6	con2i 141	. . . . . . . . . 10 ⊢ (𝜓 → ¬ 𝜑)
8	4, 7	jaoi 857	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) → ¬ 𝜑)
9	8	con2i 141	. . . . . . . 8 ⊢ (𝜑 → ¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜓))
10	4	con2i 141	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ¬ (𝜑 ∨ 𝜓))
11	10	bianfd 538	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝜑 ∨ 𝜓) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
12	6	bianfd 538	. . . . . . . . 9 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
13	11, 12	orbi12d 919	. . . . . . . 8 ⊢ (𝜑 → ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
14	9, 13	mtbid 327	. . . . . . 7 ⊢ (𝜑 → ¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
15		biorf 937	. . . . . . 7 ⊢ (¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
17	3, 16	bitrd 282	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
18		3orrot 1094	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
19		df-3or 1090	. . . . . 6 ⊢ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
20	18, 19	bitri 278	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
21	17, 20	bitr4di 292	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
22	21	eubidv 2585	. . 3 ⊢ (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
23	2, 22	mpbii 236	. 2 ⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
24		eueq3.3	. . . 4 ⊢ 𝐶 ∈ V
25	24	eueqi 3611	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐶
26		ibar 532	. . . . . 6 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
27	6	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ¬ 𝜓)
28		pm2.46 883	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
29	28	adantr 484	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
30	27, 29	jaoi 857	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
31	30	con2i 141	. . . . . . 7 ⊢ (𝜓 → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
32		biorf 937	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
33	31, 32	syl 17	. . . . . 6 ⊢ (𝜓 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
34	26, 33	bitrd 282	. . . . 5 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
35		df-3or 1090	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
36	34, 35	bitr4di 292	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
37	36	eubidv 2585	. . 3 ⊢ (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
38	25, 37	mpbii 236	. 2 ⊢ (𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
39		eueq3.2	. . . 4 ⊢ 𝐵 ∈ V
40	39	eueqi 3611	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐵
41		ibar 532	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
42		simpl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
43		simpl 486	. . . . . . . 8 ⊢ ((𝜓 ∧ 𝑥 = 𝐶) → 𝜓)
44	42, 43	orim12i 909	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → (𝜑 ∨ 𝜓))
45		biorf 937	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
46	44, 45	nsyl5 162	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
47	41, 46	bitrd 282	. . . . 5 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
48		3orcomb 1096	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
49		df-3or 1090	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
50	48, 49	bitri 278	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
51	47, 50	bitr4di 292	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
52	51	eubidv 2585	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
53	40, 52	mpbii 236	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
54	23, 38, 53	ecase3 1032	1 ⊢ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 847   ∨ w3o 1088   = wceq 1543   ∈ wcel 2112  ∃!weu 2567  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-tru 1546  df-ex 1788  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400

This theorem is referenced by:  moeq3  3614