# Metamath Proof Explorer

## Theorem ralcom4

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019)

Ref Expression
Assertion ralcom4
`|- ( A. x e. A A. y ph <-> A. y A. x e. A ph )`

### Proof

Step Hyp Ref Expression
1 19.21v
` |-  ( A. y ( x e. A -> ph ) <-> ( x e. A -> A. y ph ) )`
2 1 bicomi
` |-  ( ( x e. A -> A. y ph ) <-> A. y ( x e. A -> ph ) )`
3 2 albii
` |-  ( A. x ( x e. A -> A. y ph ) <-> A. x A. y ( x e. A -> ph ) )`
4 alcom
` |-  ( A. x A. y ( x e. A -> ph ) <-> A. y A. x ( x e. A -> ph ) )`
5 3 4 bitri
` |-  ( A. x ( x e. A -> A. y ph ) <-> A. y A. x ( x e. A -> ph ) )`
6 df-ral
` |-  ( A. x e. A A. y ph <-> A. x ( x e. A -> A. y ph ) )`
7 df-ral
` |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )`
8 7 albii
` |-  ( A. y A. x e. A ph <-> A. y A. x ( x e. A -> ph ) )`
9 5 6 8 3bitr4i
` |-  ( A. x e. A A. y ph <-> A. y A. x e. A ph )`