Metamath Proof Explorer

Theorem rspccv

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006)

Ref Expression
Hypothesis rspcv.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion rspccv 
|- ( A. x e. B ph -> ( A e. B -> ps ) )

Proof

Step Hyp Ref Expression
1 rspcv.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 1 rspcv 
 |-  ( A e. B -> ( A. x e. B ph -> ps ) )
3 2 com12 
 |-  ( A. x e. B ph -> ( A e. B -> ps ) )