Theorem ralcom3

Description: A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Assertion	ralcom3	|- ( A. x e. A ( x e. B -> ph ) <-> A. x e. B ( x e. A -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.04	|- ( ( x e. A -> ( x e. B -> ph ) ) -> ( x e. B -> ( x e. A -> ph ) ) )
2	1	ralimi2	|- ( A. x e. A ( x e. B -> ph ) -> A. x e. B ( x e. A -> ph ) )
3		pm2.04	|- ( ( x e. B -> ( x e. A -> ph ) ) -> ( x e. A -> ( x e. B -> ph ) ) )
4	3	ralimi2	|- ( A. x e. B ( x e. A -> ph ) -> A. x e. A ( x e. B -> ph ) )
5	2 4	impbii	|- ( A. x e. A ( x e. B -> ph ) <-> A. x e. B ( x e. A -> ph ) )