Metamath Proof Explorer

Theorem rspesbca

Description: Existence form of rspsbca . (Contributed by NM, 29-Feb-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion rspesbca 
|- ( ( A e. B /\ [. A / x ]. ph ) -> E. x e. B ph )

Proof

Step Hyp Ref Expression
1 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2 1 rspcev 
 |-  ( ( A e. B /\ [. A / x ]. ph ) -> E. y e. B [ y / x ] ph )
3 cbvrexsvw 
 |-  ( E. x e. B ph <-> E. y e. B [ y / x ] ph )
4 2 3 sylibr 
 |-  ( ( A e. B /\ [. A / x ]. ph ) -> E. x e. B ph )