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	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ∀∃ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		2alsraln0	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ∀∃ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ) )
2		pm4.24	⊢ ( 𝐴 ≠ ∅ ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) )
3	2	bicomi	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ↔ 𝐴 ≠ ∅ )
4	3	anbi2i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) )
5	1 4	bitri	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ∀∃ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) )