# Metamath Proof Explorer

## Theorem ralbidar

Description: More general form of ralbida . (Contributed by Andrew Salmon, 25-Jul-2011)

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

### Proof

Step Hyp Ref Expression
1 ralbidar.1 ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
2 ralbidar.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\psi }↔{\chi }\right)$
3 2 ex ${⊢}{\phi }\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)$
4 3 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)$
5 1 4 syl ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)$
6 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)\right)$
7 5 6 sylib ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)\right)$
8 pm2.43 ${⊢}\left({x}\in {A}\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)\right)\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)$
9 8 pm5.74d ${⊢}\left({x}\in {A}\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)\right)\to \left(\left({x}\in {A}\to {\psi }\right)↔\left({x}\in {A}\to {\chi }\right)\right)$
10 9 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {\psi }\right)↔\left({x}\in {A}\to {\chi }\right)\right)$
11 albi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {\psi }\right)↔\left({x}\in {A}\to {\chi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)\right)$
12 7 10 11 3syl ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)\right)$
13 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)$
14 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)$
15 12 13 14 3bitr4g ${⊢}{\phi }\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$