# Metamath Proof Explorer

## Theorem ralprgf

Description: Convert a restricted universal quantification over a pair to a conjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011) (Revised by AV, 8-Apr-2023)

Ref Expression
Hypotheses ralprgf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
ralprgf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
ralprgf.a ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
ralprgf.b ${⊢}{x}={B}\to \left({\phi }↔{\chi }\right)$
Assertion ralprgf ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔\left({\psi }\wedge {\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 ralprgf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 ralprgf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
3 ralprgf.a ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
4 ralprgf.b ${⊢}{x}={B}\to \left({\phi }↔{\chi }\right)$
5 df-pr ${⊢}\left\{{A},{B}\right\}=\left\{{A}\right\}\cup \left\{{B}\right\}$
6 5 raleqi ${⊢}\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in \left(\left\{{A}\right\}\cup \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }$
7 ralunb ${⊢}\forall {x}\in \left(\left\{{A}\right\}\cup \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 6 7 bitri ${⊢}\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 1 3 ralsngf ${⊢}{A}\in {V}\to \left(\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔{\psi }\right)$
10 2 4 ralsngf ${⊢}{B}\in {W}\to \left(\forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔{\chi }\right)$
11 9 10 bi2anan9 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left(\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left({\psi }\wedge {\chi }\right)\right)$
12 8 11 syl5bb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔\left({\psi }\wedge {\chi }\right)\right)$