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	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
Assertion	r2allem	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		r2allem.1	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 ) )
3		impexp	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
4	3	albii	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
5		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) )
6	5	imbi2i	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
7	1 4 6	3bitr4i	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 ) )
8	7	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 ) )
9	2 8	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) )