Theorem exsbim

Description: One direction of the equivalence in exsb is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

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

Proof

Step	Hyp	Ref	Expression
1		alequexv	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 𝜑 )
2	1	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 𝜑 )