# Metamath Proof Explorer

## Theorem 2ralbidva

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019)

Ref Expression
Hypothesis 2ralbidva.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({\psi }↔{\chi }\right)$
Assertion 2ralbidva ${⊢}{\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 2ralbidva.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({\psi }↔{\chi }\right)$
2 1 anassrs ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\to \left({\psi }↔{\chi }\right)$
3 2 ralbidva ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 ralbidva ${⊢}{\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)$