# Metamath Proof Explorer

## Theorem 2ralbidv

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006) (Revised by Szymon Jaroszewicz, 16-Mar-2007)

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

### Proof

Step Hyp Ref Expression
1 2ralbidv.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 1 ralbidv ${⊢}{\phi }\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
3 2 ralbidv ${⊢}{\phi }\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$