Theorem dfmoeu 2534

Description: An elementary proof of moeu 2581 in disguise, connecting an expression characterizing uniqueness (df-mo 2538) to that of existential uniqueness (eu6 2572). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2535. (Contributed by Wolf Lammen, 27-May-2019.)

Assertion

Ref	Expression
dfmoeu	⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem dfmoeu

Step	Hyp	Ref	Expression
1		alnex 1778	. . . . 5 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		pm2.21 123	. . . . . 6 ⊢ (¬ 𝜑 → (𝜑 → 𝑥 = 𝑦))
3	2	alimi 1808	. . . . 5 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	1, 3	sylbir 235	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
5	4	19.8ad 2180	. . 3 ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
6		biimp 215	. . . . 5 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
7	6	alimi 1808	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
8	7	eximi 1832	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
9	5, 8	ja 186	. 2 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
10		nfia1 2151	. . . . 5 ⊢ Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
11		id 22	. . . . . . . . 9 ⊢ (𝜑 → 𝜑)
12		ax12v 2176	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
13	12	com12 32	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
14	11, 13	embantd 59	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
15	14	spsd 2185	. . . . . . 7 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
16	15	ancld 550	. . . . . 6 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))))
17		albiim 1887	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18	16, 17	imbitrrdi 252	. . . . 5 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
19	10, 18	exlimi 2215	. . . 4 ⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
20	19	eximdv 1915	. . 3 ⊢ (∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
21	20	com12 32	. 2 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
22	9, 21	impbii 209	1 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781

This theorem is referenced by:  dfeumo  2535  eu6  2572  dfmo  2594