Description: Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2Sep2022)
Ref  Expression  

Hypothesis  rspceeqv.1   ( x = A > C = D ) 

Assertion  rspceeqv   ( ( A e. B /\ E = D ) > E. x e. B E = C ) 
Step  Hyp  Ref  Expression 

1  rspceeqv.1   ( x = A > C = D ) 

2  1  eqeq2d   ( x = A > ( E = C <> E = D ) ) 
3  2  rspcev   ( ( A e. B /\ E = D ) > E. x e. B E = C ) 