Metamath Proof Explorer

Theorem 2alsraln0id

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

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

Proof

Step Hyp Ref Expression
1 2alsraln0 ⊢ ∀∃ x x ∈ A → ∀∃ y y ∈ A → φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ A ≠ ∅ ∧ A ≠ ∅
2 pm4.24 ⊢ A ≠ ∅ ↔ A ≠ ∅ ∧ A ≠ ∅
3 2 bicomi ⊢ A ≠ ∅ ∧ A ≠ ∅ ↔ A ≠ ∅
4 3 anbi2i ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ A ≠ ∅ ∧ A ≠ ∅ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ A ≠ ∅
5 1 4 bitri ⊢ ∀∃ x x ∈ A → ∀∃ y y ∈ A → φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ A ≠ ∅