Theorem eueq3 3700

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 3698	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐴
3		ibar 528	. . . . . 6 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (𝜑 ∧ 𝑥 = 𝐴)))
4		pm2.45 878	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
5		eueq3.4	. . . . . . . . . . . 12 ⊢ ¬ (𝜑 ∧ 𝜓)
6	5	imnani 400	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝜓)
7	6	con2i 139	. . . . . . . . . 10 ⊢ (𝜓 → ¬ 𝜑)
8	4, 7	jaoi 854	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) → ¬ 𝜑)
9	8	con2i 139	. . . . . . . 8 ⊢ (𝜑 → ¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜓))
10	4	con2i 139	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ¬ (𝜑 ∨ 𝜓))
11	10	bianfd 534	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝜑 ∨ 𝜓) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
12	6	bianfd 534	. . . . . . . . 9 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
13	11, 12	orbi12d 915	. . . . . . . 8 ⊢ (𝜑 → ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
14	9, 13	mtbid 324	. . . . . . 7 ⊢ (𝜑 → ¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
15		biorf 933	. . . . . . 7 ⊢ (¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
16	14, 15	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
17	3, 16	bitrd 279	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
18		3orrot 1089	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
19		df-3or 1085	. . . . . 6 ⊢ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
20	18, 19	bitri 275	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
21	17, 20	bitr4di 289	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
22	21	eubidv 2572	. . 3 ⊢ (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
23	2, 22	mpbii 232	. 2 ⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
24		eueq3.3	. . . 4 ⊢ 𝐶 ∈ V
25	24	eueqi 3698	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐶
26		ibar 528	. . . . . 6 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
27	6	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ¬ 𝜓)
28		pm2.46 879	. . . . . . . . . 10 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
29	28	adantr 480	. . . . . . . . 9 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
30	27, 29	jaoi 854	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
31	30	con2i 139	. . . . . . 7 ⊢ (𝜓 → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
32		biorf 933	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
33	31, 32	syl 17	. . . . . 6 ⊢ (𝜓 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
34	26, 33	bitrd 279	. . . . 5 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
35		df-3or 1085	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
36	34, 35	bitr4di 289	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
37	36	eubidv 2572	. . 3 ⊢ (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
38	25, 37	mpbii 232	. 2 ⊢ (𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
39		eueq3.2	. . . 4 ⊢ 𝐵 ∈ V
40	39	eueqi 3698	. . 3 ⊢ ∃!𝑥 𝑥 = 𝐵
41		ibar 528	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
42		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
43		simpl 482	. . . . . . . 8 ⊢ ((𝜓 ∧ 𝑥 = 𝐶) → 𝜓)
44	42, 43	orim12i 905	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → (𝜑 ∨ 𝜓))
45		biorf 933	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
46	44, 45	nsyl5 159	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
47	41, 46	bitrd 279	. . . . 5 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
48		3orcomb 1091	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
49		df-3or 1085	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
50	48, 49	bitri 275	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
51	47, 50	bitr4di 289	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
52	51	eubidv 2572	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
53	40, 52	mpbii 232	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
54	23, 38, 53	ecase3 1028	1 ⊢ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098  ∃!weu 2554  Vcvv 3466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-tru 1536  df-ex 1774  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468

This theorem is referenced by:  moeq3  3701