Theorem dfmoeu 2561

Description: An elementary proof of moeu 2609 in disguise, connecting an expression characterizing uniqueness (df-mo 2565) to that of existential uniqueness (eu6 2600). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2562. (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 1809	. . . . 5 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		pm2.21 124	. . . . . 6 ⊢ (¬ 𝜑 → (𝜑 → 𝑥 = 𝑦))
3	2	alimi 1839	. . . . 5 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	1, 3	sylbir 238	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
5	4	19.8ad 2216	. . 3 ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
6		biimp 218	. . . . 5 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
7	6	alimi 1839	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
8	7	eximi 1863	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
9	5, 8	ja 188	. 2 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
10		nfia1 2186	. . . . 5 ⊢ Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
11		id 23	. . . . . . . . 9 ⊢ (𝜑 → 𝜑)
12		ax12v 2212	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
13	12	com12 33	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
14	11, 13	embantd 60	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
15	14	spsd 2221	. . . . . . 7 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
16	15	ancld 559	. . . . . 6 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))))
17		albiim 1917	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18	16, 17	imbitrrdi 255	. . . . 5 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
19	10, 18	exlimi 2251	. . . 4 ⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
20	19	eximdv 1945	. . 3 ⊢ (∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
21	20	com12 33	. 2 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
22	9, 21	impbii 212	1 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1566  ∃wex 1807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-10 2174  ax-12 2211

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-nf 1812

This theorem is referenced by:  dfeumo  2562  eu6  2600  dfmo2  2622