Theorem eu6OLD 2594

Description: Obsolete version of eu6 2592 as of 28-Dec-2022. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2587 was then proved as dfeu 2614. (Revised by BJ, 30-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
eu6OLD	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6OLD

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-eu 2587	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		exsb 2327	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
3		df-mo 2551	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
4	2, 3	anbi12i 620	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
5		exdistrv 1998	. . . 4 ⊢ (∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
6		19.26 1916	. . . . . . . 8 ⊢ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
7		pm3.33 755	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) → (𝑥 = 𝑦 → 𝑥 = 𝑧))
8	7	pm4.71i 555	. . . . . . . . . 10 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ↔ (((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ (𝑥 = 𝑦 → 𝑥 = 𝑧)))
9	8	albii 1863	. . . . . . . . 9 ⊢ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ↔ ∀𝑥(((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ (𝑥 = 𝑦 → 𝑥 = 𝑧)))
10		19.26 1916	. . . . . . . . 9 ⊢ (∀𝑥(((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ (𝑥 = 𝑦 → 𝑥 = 𝑧)) ↔ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧)))
11		equvelv 2080	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) ↔ 𝑦 = 𝑧)
12	6, 11	anbi12i 620	. . . . . . . . . 10 ⊢ ((∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧)) ↔ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧))
13		anass 462	. . . . . . . . . . 11 ⊢ (((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑧) ∧ 𝑦 = 𝑧)))
14		equequ2 2073	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
15	14	bicomd 215	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦))
16	15	imbi2d 332	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜑 → 𝑥 = 𝑦)))
17	16	albidv 1963	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑦)))
18	17	pm5.32ri 571	. . . . . . . . . . . 12 ⊢ ((∀𝑥(𝜑 → 𝑥 = 𝑧) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
19	18	anbi2i 616	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑧) ∧ 𝑦 = 𝑧)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ 𝑦 = 𝑧)))
20	13, 19	bitri 267	. . . . . . . . . 10 ⊢ (((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ 𝑦 = 𝑧)))
21		anass 462	. . . . . . . . . . 11 ⊢ (((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ 𝑦 = 𝑧)))
22		19.26 1916	. . . . . . . . . . . . 13 ⊢ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑦)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)))
23		ancom 454	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑦)) ↔ ((𝜑 → 𝑥 = 𝑦) ∧ (𝑥 = 𝑦 → 𝜑)))
24		dfbi2 468	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) ↔ ((𝜑 → 𝑥 = 𝑦) ∧ (𝑥 = 𝑦 → 𝜑)))
25	24	bicomi 216	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 → 𝑥 = 𝑦) ∧ (𝑥 = 𝑦 → 𝜑)) ↔ (𝜑 ↔ 𝑥 = 𝑦))
26	23, 25	bitri 267	. . . . . . . . . . . . . 14 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑦)) ↔ (𝜑 ↔ 𝑥 = 𝑦))
27	26	albii 1863	. . . . . . . . . . . . 13 ⊢ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑦)) ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
28	22, 27	bitr3i 269	. . . . . . . . . . . 12 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
29	28	anbi1i 617	. . . . . . . . . . 11 ⊢ (((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
30	21, 29	bitr3i 269	. . . . . . . . . 10 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ 𝑦 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
31	12, 20, 30	3bitri 289	. . . . . . . . 9 ⊢ ((∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ∧ ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
32	9, 10, 31	3bitri 289	. . . . . . . 8 ⊢ (∀𝑥((𝑥 = 𝑦 → 𝜑) ∧ (𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
33	6, 32	bitr3i 269	. . . . . . 7 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
34	33	exbii 1892	. . . . . 6 ⊢ (∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
35		19.42v 1996	. . . . . 6 ⊢ (∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
36	34, 35	bitri 267	. . . . 5 ⊢ (∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
37	36	exbii 1892	. . . 4 ⊢ (∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
38	5, 37	bitr3i 269	. . 3 ⊢ ((∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
39		ax6evr 2062	. . . . . 6 ⊢ ∃𝑧 𝑦 = 𝑧
40	39	biantru 525	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
41	40	bicomi 216	. . . 4 ⊢ ((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧) ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
42	41	exbii 1892	. . 3 ⊢ (∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
43	38, 42	bitri 267	. 2 ⊢ ((∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
44	1, 4, 43	3bitri 289	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599  ∃wex 1823  ∃*wmo 2549  ∃!weu 2586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-11 2150  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-mo 2551  df-eu 2587

This theorem is referenced by: (None)