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

Metamath Proof Explorer

Theorem spsbe

Description: Existential generalization: if a proposition is true for a specific instance, then there exists an instance where it is true. (Contributed by NM, 29-Jun-1993) (Proof shortened by Wolf Lammen, 3-May-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Steven Nguyen, 11-Jul-2023)

Ref Expression
Assertion spsbe 
|- ( [ t / x ] ph -> E. x ph )

Proof

Step Hyp Ref Expression
1 dfsb 
 |-  ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
2 alequexv 
 |-  ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> E. y A. x ( x = y -> ph ) )
3 1 2 sylbi 
 |-  ( [ t / x ] ph -> E. y A. x ( x = y -> ph ) )
4 exsbim 
 |-  ( E. y A. x ( x = y -> ph ) -> E. x ph )
5 3 4 syl 
 |-  ( [ t / x ] ph -> E. x ph )