# Metamath Proof Explorer

## Theorem r2allem

Description: Lemma factoring out common proof steps of r2alf and r2al . Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020)

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

### Proof

Step Hyp Ref Expression
1 r2allem.1 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({y}\in {B}\to {\phi }\right)\right)↔\left({x}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {\phi }\right)\right)$
2 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 impexp ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)↔\left({x}\in {A}\to \left({y}\in {B}\to {\phi }\right)\right)$
4 3 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({y}\in {B}\to {\phi }\right)\right)$
5 df-ral ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {\phi }\right)$
6 5 imbi2i ${⊢}\left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left({x}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {\phi }\right)\right)$
7 1 4 6 3bitr4i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)↔\left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 7 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 2 8 bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)$