# Metamath Proof Explorer

## Theorem ralcom

Description: Commutation of restricted universal quantifiers. See ralcom2 for a version without disjoint variable condition on x , y . This theorem should be used in place of ralcom2 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion ralcom ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 ancomst ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to {\phi }\right)↔\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)$
2 1 2albii ${⊢}\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}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)$
3 alcom ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)$
4 2 3 bitri ${⊢}\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 {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)$
5 r2al ${⊢}\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)$
6 r2al ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\wedge {x}\in {A}\right)\to {\phi }\right)$
7 4 5 6 3bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$