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 ) |
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 ) |