Theorem alsralrex

Description: The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and some x in A satisfies ph . (Contributed by Peter Mazsa, 27-Nov-2018) (Revised by David A. Wheeler, 15-Jul-2026)

	Ref	Expression
Assertion	alsralrex	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-als	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3	2	bicomi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
4	3	anbi1i	⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
5		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
6	5	biimpri	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
7		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑥 ∈ 𝐴 𝜑 )
8	6 7	sylan	⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑥 ∈ 𝐴 𝜑 )
9	8	expcom	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
10		rexn0	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ )
11	5	biimpi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 )
12	10 11	syl	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
13	12	a1i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 ) )
14	9 13	impbid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
15	14	pm5.32i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
16	4 15	bitri	⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
17	1 16	bitri	⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )