Theorem eu6im

Description: One direction of eu6 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

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

Proof

Step	Hyp	Ref	Expression
1		exsbim	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 𝜑 )
2	1	anim1i	⊢ ( ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
3		eu6lem	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
4		eu3v	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
5	2 3 4	3imtr4i	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃! 𝑥 𝜑 )