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 A is not empty. (Contributed by Peter Mazsa, 28-Nov-2018) (Revised by David A. Wheeler, 15-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | alsraln0 | ⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alsralrex | ⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 2 | rexn0 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ ) | |
| 3 | 2 | a1i | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ ) ) |
| 4 | r19.2z | ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑥 ∈ 𝐴 𝜑 ) | |
| 5 | 4 | expcom | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 𝜑 ) ) |
| 6 | 3 5 | impbid | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅ ) ) |
| 7 | 6 | pm5.32i | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) ) |
| 8 | 1 7 | bitri | ⊢ ( ∀∃ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅ ) ) |