Theorem eu6lem 2573

Description: Lemma of eu6im 2575. A dissection of an idiom characterizing existential uniqueness. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2569 was then proved as dfeu 2595. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023.)

Assertion

Ref	Expression
eu6lem	⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))

Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦,𝑧

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6lem

Step	Hyp	Ref	Expression
1		19.42v 1957	. . . 4 ⊢ (∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
2		alsyl 1896	. . . . . . . 8 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧))
3		equvelv 2034	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) ↔ 𝑦 = 𝑧)
4	2, 3	sylib 217	. . . . . . 7 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) → 𝑦 = 𝑧)
5	4	pm4.71i 560	. . . . . 6 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧))
6		albiim 1892	. . . . . . . . 9 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
7	6	biancomi 463	. . . . . . . 8 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)))
8		equequ2 2029	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
9	8	imbi2d 341	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜑 → 𝑥 = 𝑧)))
10	9	albidv 1923	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
11	10	anbi2d 629	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧))))
12	7, 11	bitrid 282	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧))))
13	12	pm5.32ri 576	. . . . . 6 ⊢ ((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧) ↔ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧))
14	5, 13	bitr4i 277	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
15	14	exbii 1850	. . . 4 ⊢ (∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
16		ax6evr 2018	. . . . 5 ⊢ ∃𝑧 𝑦 = 𝑧
17	16	biantru 530	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
18	1, 15, 17	3bitr4ri 304	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
19	18	exbii 1850	. 2 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
20		exdistrv 1959	. 2 ⊢ (∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
21	19, 20	bitri 274	1 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  eu6im  2575