# Metamath Proof Explorer

## Theorem rspc2v

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999)

Ref Expression
Hypotheses rspc2v.1 ${⊢}{x}={A}\to \left({\phi }↔{\chi }\right)$
rspc2v.2 ${⊢}{y}={B}\to \left({\chi }↔{\psi }\right)$
Assertion rspc2v ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 rspc2v.1 ${⊢}{x}={A}\to \left({\phi }↔{\chi }\right)$
2 rspc2v.2 ${⊢}{y}={B}\to \left({\chi }↔{\psi }\right)$
3 1 ralbidv ${⊢}{x}={A}\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 rspcv ${⊢}{A}\in {C}\to \left(\forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 2 rspcv ${⊢}{B}\in {D}\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\to {\psi }\right)$
6 4 5 sylan9 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$