Metamath Proof Explorer


Theorem alequexv

Description: Version of equs4v with its consequence simplified by exsimpr . (Contributed by BJ, 9-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 ax6ev 𝑥 𝑥 = 𝑦
2 exim ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜑 ) )
3 1 2 mpi ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → ∃ 𝑥 𝜑 )