This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem speiv

Description: Inference from existential specialization. (Contributed by NM, 19-Aug-1993) Use spimew . (Revised by Wolf Lammen, 22-Oct-2023)

Ref Expression
Hypotheses speiv.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
speiv.2 ⊢ 𝜓
Assertion speiv ∃ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 speiv.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
2 speiv.2 ⊢ 𝜓
3 2 hbth ⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
4 3 1 spimew ⊢ ( 𝜓 → ∃ 𝑥 𝜑 )
5 2 4 ax-mp ⊢ ∃ 𝑥 𝜑