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

Proof

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