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

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 )
2		alsraln0	⊢ ( ∀∃ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) )
3	1 2	alsbii	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ∀∃ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ↔ ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ) )
4		alsraln0	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) )
5		r19.27zv	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ) )
6	5	pm5.32ri	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) )
7		anass	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ) )
8		ancom	⊢ ( ( 𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ↔ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
9	8	anbi2i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
10	7 9	bitri	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
11	6 10	bitri	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝐴 ≠ ∅ ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
12	4 11	bitri	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 𝜑 ∧ 𝐵 ≠ ∅ ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
13	3 12	bitri	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → ∀∃ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )