Metamath Proof Explorer


Theorem spimew

Description: Existential introduction, using implicit substitution. Compare Lemma 14 of Tarski p. 70. (Contributed by NM, 7-Aug-1994) (Proof shortened by Wolf Lammen, 22-Oct-2023)

Ref Expression
Hypotheses spimew.1
|- ( ph -> A. x ph )
spimew.2
|- ( x = y -> ( ph -> ps ) )
Assertion spimew
|- ( ph -> E. x ps )

Proof

Step Hyp Ref Expression
1 spimew.1
 |-  ( ph -> A. x ph )
2 spimew.2
 |-  ( x = y -> ( ph -> ps ) )
3 ax6v
 |-  -. A. x -. x = y
4 2 speimfw
 |-  ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )
5 3 1 4 mpsyl
 |-  ( ph -> E. x ps )