Theorem r2alf

Description: Double restricted universal quantification. For a version based on fewer axioms see r2al . (Contributed by Mario Carneiro, 14-Oct-2016) Use r2allem . (Revised by Wolf Lammen, 9-Jan-2020)

	Ref	Expression
Hypothesis	r2alf.1	|- F/_ y A
Assertion	r2alf	|- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		r2alf.1	|- F/_ y A
2	1	nfcri	|- F/ y x e. A
3	2	19.21	|- ( A. y ( x e. A -> ( y e. B -> ph ) ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
4	3	r2allem	|- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )