Metamath Proof Explorer

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 ⊢ ∀∃ x x ∈ A → φ ↔ ∀ x ∈ A φ ∧ ∃ x ∈ A φ

Proof

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