Theorem r2allem

Description: Lemma factoring out common proof steps of r2alf and r2al . Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020)

	Ref	Expression
Hypothesis	r2allem.1	|- ( A. y ( x e. A -> ( y e. B -> ph ) ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
Assertion	r2allem	|- ( 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		r2allem.1	|- ( A. y ( x e. A -> ( y e. B -> ph ) ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
2		df-ral	|- ( A. x e. A A. y e. B ph <-> A. x ( x e. A -> A. y e. B ph ) )
3		impexp	|- ( ( ( x e. A /\ y e. B ) -> ph ) <-> ( x e. A -> ( y e. B -> ph ) ) )
4	3	albii	|- ( A. y ( ( x e. A /\ y e. B ) -> ph ) <-> A. y ( x e. A -> ( y e. B -> ph ) ) )
5		df-ral	|- ( A. y e. B ph <-> A. y ( y e. B -> ph ) )
6	5	imbi2i	|- ( ( x e. A -> A. y e. B ph ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
7	1 4 6	3bitr4i	|- ( A. y ( ( x e. A /\ y e. B ) -> ph ) <-> ( x e. A -> A. y e. B ph ) )
8	7	albii	|- ( A. x A. y ( ( x e. A /\ y e. B ) -> ph ) <-> A. x ( x e. A -> A. y e. B ph ) )
9	2 8	bitr4i	|- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )