Metamath Proof Explorer

Theorem 2alsraln0

Description: Nested general "all some" quantifiers with class membership as their antecedents: ph holds for every x in A and every y in B , and both A and B are not empty. (Contributed by Peter Mazsa, 28-May-2019) (Revised by David A. Wheeler, 15-Jul-2026)

Ref Expression
Assertion 2alsraln0 ⊢ ∀∃ x x ∈ A → ∀∃ y y ∈ B → φ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅

Proof

Step Hyp Ref Expression
1 biid ⊢ x ∈ A ↔ x ∈ A
2 alsraln0 ⊢ ∀∃ y y ∈ B → φ ↔ ∀ y ∈ B φ ∧ B ≠ ∅
3 1 2 alsbii ⊢ ∀∃ x x ∈ A → ∀∃ y y ∈ B → φ ↔ ∀∃ x x ∈ A → ∀ y ∈ B φ ∧ B ≠ ∅
4 alsraln0 ⊢ ∀∃ x x ∈ A → ∀ y ∈ B φ ∧ B ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅
5 r19.27zv ⊢ A ≠ ∅ → ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅
6 5 pm5.32ri ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅
7 anass ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅
8 ancom ⊢ B ≠ ∅ ∧ A ≠ ∅ ↔ A ≠ ∅ ∧ B ≠ ∅
9 8 anbi2i ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅
10 7 9 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅
11 6 10 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ B ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅
12 4 11 bitri ⊢ ∀∃ x x ∈ A → ∀ y ∈ B φ ∧ B ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅
13 3 12 bitri ⊢ ∀∃ x x ∈ A → ∀∃ y y ∈ B → φ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ A ≠ ∅ ∧ B ≠ ∅