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) (Proof shortened by Wolf Lammen, 31-Oct-2024)

	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	albii	|- ( A. x A. y ( x e. A -> ph ) <-> A. x ( x e. A -> A. y ph ) )
3		alcom	|- ( A. y A. x ( x e. A -> ph ) <-> A. x A. y ( x e. A -> ph ) )
4		df-ral	|- ( A. x e. A A. y ph <-> A. x ( x e. A -> A. y ph ) )
5	2 3 4	3bitr4ri	|- ( A. x e. A A. y ph <-> A. y A. x ( x e. A -> ph ) )
6		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
7	6	albii	|- ( A. y A. x e. A ph <-> A. y A. x ( x e. A -> ph ) )
8	5 7	bitr4i	|- ( A. x e. A A. y ph <-> A. y A. x e. A ph )