Metamath Proof Explorer


Theorem rspc2dv

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025)

Ref Expression
Hypotheses rspc2dv.1
|- ( x = A -> ( ps <-> th ) )
rspc2dv.2
|- ( y = B -> ( th <-> ch ) )
rspc2dv.3
|- ( ph -> A. x e. C A. y e. D ps )
rspc2dv.4
|- ( ph -> A e. C )
rspc2dv.5
|- ( ph -> B e. D )
Assertion rspc2dv
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 rspc2dv.1
 |-  ( x = A -> ( ps <-> th ) )
2 rspc2dv.2
 |-  ( y = B -> ( th <-> ch ) )
3 rspc2dv.3
 |-  ( ph -> A. x e. C A. y e. D ps )
4 rspc2dv.4
 |-  ( ph -> A e. C )
5 rspc2dv.5
 |-  ( ph -> B e. D )
6 1 2 rspc2va
 |-  ( ( ( A e. C /\ B e. D ) /\ A. x e. C A. y e. D ps ) -> ch )
7 4 5 3 6 syl21anc
 |-  ( ph -> ch )