# Metamath Proof Explorer

## Theorem ralcom4f

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypothesis ralcom4f.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
Assertion ralcom4f ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 ralcom4f.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
2 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{V}$
3 1 2 ralcomf ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
4 ralv ${⊢}\forall {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 ralv ${⊢}\forall {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
7 3 5 6 3bitr3i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$