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 ⊢ x = y → ψ → φ
speiv.2 ⊢ ψ
Assertion speiv ⊢ ∃ x φ

Proof

Step Hyp Ref Expression
1 speiv.1 ⊢ x = y → ψ → φ
2 speiv.2 ⊢ ψ
3 2 hbth ⊢ ψ → ∀ x ψ
4 3 1 spimew ⊢ ψ → ∃ x φ
5 2 4 ax-mp ⊢ ∃ x φ