Metamath Proof Explorer

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 ⊢ ∀ y x ∈ A → y ∈ B → φ ↔ x ∈ A → ∀ y y ∈ B → φ
Assertion r2allem ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ

Proof

Step Hyp Ref Expression
1 r2allem.1 ⊢ ∀ y x ∈ A → y ∈ B → φ ↔ x ∈ A → ∀ y y ∈ B → φ
2 df-ral ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x x ∈ A → ∀ y ∈ B φ
3 impexp ⊢ x ∈ A ∧ y ∈ B → φ ↔ x ∈ A → y ∈ B → φ
4 3 albii ⊢ ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ y x ∈ A → y ∈ B → φ
5 df-ral ⊢ ∀ y ∈ B φ ↔ ∀ y y ∈ B → φ
6 5 imbi2i ⊢ x ∈ A → ∀ y ∈ B φ ↔ x ∈ A → ∀ y y ∈ B → φ
7 1 4 6 3bitr4i ⊢ ∀ y x ∈ A ∧ y ∈ B → φ ↔ x ∈ A → ∀ y ∈ B φ
8 7 albii ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ x x ∈ A → ∀ y ∈ B φ
9 2 8 bitr4i ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ