Theorem eueq3 3704

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 3702	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐴
3		ibar 531	. . . . . 6 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (𝜑 ∧ 𝑥 = 𝐴)))
4		pm2.45 878	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
5		eueq3.4	. . . . . . . . . . . 12 ⊢ ¬ (𝜑 ∧ 𝜓)
6	5	imnani 403	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝜓)
7	6	con2i 141	. . . . . . . . . 10 ⊢ (𝜓 → ¬ 𝜑)
8	4, 7	jaoi 853	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) → ¬ 𝜑)
9	8	con2i 141	. . . . . . . 8 ⊢ (𝜑 → ¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜓))
10	4	con2i 141	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ¬ (𝜑 ∨ 𝜓))
11	10	bianfd 537	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝜑 ∨ 𝜓) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
12	6	bianfd 537	. . . . . . . . 9 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
13	11, 12	orbi12d 915	. . . . . . . 8 ⊢ (𝜑 → ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
14	9, 13	mtbid 326	. . . . . . 7 ⊢ (𝜑 → ¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
15		biorf 933	. . . . . . 7 ⊢ (¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
17	3, 16	bitrd 281	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
18		3orrot 1088	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
19		df-3or 1084	. . . . . 6 ⊢ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
20	18, 19	bitri 277	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
21	17, 20	syl6bbr 291	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
22	21	eubidv 2672	. . 3 ⊢ (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
23	2, 22	mpbii 235	. 2 ⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
24		eueq3.3	. . . 4 ⊢ 𝐶 ∈ V
25	24	eueqi 3702	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐶
26		ibar 531	. . . . . 6 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
27	6	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ¬ 𝜓)
28		pm2.46 879	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
29	28	adantr 483	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
30	27, 29	jaoi 853	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
31	30	con2i 141	. . . . . . 7 ⊢ (𝜓 → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
32		biorf 933	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
33	31, 32	syl 17	. . . . . 6 ⊢ (𝜓 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
34	26, 33	bitrd 281	. . . . 5 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
35		df-3or 1084	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
36	34, 35	syl6bbr 291	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
37	36	eubidv 2672	. . 3 ⊢ (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
38	25, 37	mpbii 235	. 2 ⊢ (𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
39		eueq3.2	. . . 4 ⊢ 𝐵 ∈ V
40	39	eueqi 3702	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐵
41		ibar 531	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
42		simpl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
43		simpl 485	. . . . . . . . 9 ⊢ ((𝜓 ∧ 𝑥 = 𝐶) → 𝜓)
44	42, 43	orim12i 905	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → (𝜑 ∨ 𝜓))
45	44	con3i 157	. . . . . . 7 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
46		biorf 933	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
47	45, 46	syl 17	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
48	41, 47	bitrd 281	. . . . 5 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
49		3orcomb 1090	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
50		df-3or 1084	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
51	49, 50	bitri 277	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
52	48, 51	syl6bbr 291	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
53	52	eubidv 2672	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
54	40, 53	mpbii 235	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
55	23, 38, 54	ecase3 1027	1 ⊢ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∨ w3o 1082   = wceq 1537   ∈ wcel 2114  ∃!weu 2653  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-ex 1781  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498

This theorem is referenced by:  moeq3  3705