Metamath Proof Explorer

Theorem spesbc

Description: Existence form of spsbc . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Assertion spesbc 
|- ( [. A / x ]. ph -> E. x ph )

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. ph -> A e. _V )
2 rspesbca 
 |-  ( ( A e. _V /\ [. A / x ]. ph ) -> E. x e. _V ph )
3 1 2 mpancom 
 |-  ( [. A / x ]. ph -> E. x e. _V ph )
4 rexv 
 |-  ( E. x e. _V ph <-> E. x ph )
5 3 4 sylib 
 |-  ( [. A / x ]. ph -> E. x ph )