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 )