Metamath Proof Explorer


Theorem rspcdva

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020)

Ref Expression
Hypotheses rspcdva.1
|- ( x = C -> ( ps <-> ch ) )
rspcdva.2
|- ( ph -> A. x e. A ps )
rspcdva.3
|- ( ph -> C e. A )
Assertion rspcdva
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 rspcdva.1
 |-  ( x = C -> ( ps <-> ch ) )
2 rspcdva.2
 |-  ( ph -> A. x e. A ps )
3 rspcdva.3
 |-  ( ph -> C e. A )
4 1 rspcv
 |-  ( C e. A -> ( A. x e. A ps -> ch ) )
5 3 2 4 sylc
 |-  ( ph -> ch )