Theorem eu6lem 2652

Description: Lemma of eu6im 2654. 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 2648 was then proved as dfeu 2675. (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 1948	. . . 4 ⊢ (∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
2		alsyl 1888	. . . . . . . 8 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧))
3		equvelv 2032	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) ↔ 𝑦 = 𝑧)
4	2, 3	sylib 220	. . . . . . 7 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) → 𝑦 = 𝑧)
5	4	pm4.71i 562	. . . . . 6 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧))
6		albiim 1884	. . . . . . . . 9 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
7	6	biancomi 465	. . . . . . . 8 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)))
8		equequ2 2027	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
9	8	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜑 → 𝑥 = 𝑧)))
10	9	albidv 1915	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
11	10	anbi2d 630	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧))))
12	7, 11	syl5bb 285	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧))))
13	12	pm5.32ri 578	. . . . . 6 ⊢ ((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧) ↔ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ∧ 𝑦 = 𝑧))
14	5, 13	bitr4i 280	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
15	14	exbii 1842	. . . 4 ⊢ (∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ ∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝑦 = 𝑧))
16		ax6evr 2016	. . . . 5 ⊢ ∃𝑧 𝑦 = 𝑧
17	16	biantru 532	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑧 𝑦 = 𝑧))
18	1, 15, 17	3bitr4ri 306	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
19	18	exbii 1842	. 2 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
20		exdistrv 1950	. 2 ⊢ (∃𝑦∃𝑧(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
21	19, 20	bitri 277	1 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1529  ∃wex 1774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775

This theorem is referenced by:  eu6im  2654