Theorem dfmoeu 2562

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  dfeumo  2563  eu6  2601  dfmo2  2623