Theorem dfmoeu

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

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

Proof

Step	Hyp	Ref	Expression
1		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝑥 = 𝑦 ) )
3	2	alimi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
4	1 3	sylbir	⊢ ( ¬ ∃ 𝑥 𝜑 → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
5	4	19.8ad	⊢ ( ¬ ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6		biimp	⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
7	6	alimi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
8	7	eximi	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
9	5 8	ja	⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
10		nfia1	⊢ Ⅎ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
11		id	⊢ ( 𝜑 → 𝜑 )
12		ax12v	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
13	12	com12	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
14	11 13	embantd	⊢ ( 𝜑 → ( ( 𝜑 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
15	14	spsd	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
16	15	ancld	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
17		albiim	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
18	16 17	syl6ibr	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
19	10 18	exlimi	⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
20	19	eximdv	⊢ ( ∃ 𝑥 𝜑 → ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
21	20	com12	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
22	9 21	impbii	⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )