Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  df-alsc GIF version

Definition df-alsc 13689
Description: Define "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴 and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.)
Assertion
Ref Expression
df-alsc (∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))

Detailed syntax breakdown of Definition df-alsc
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3walsc 13687 . 2 wff ∀!𝑥𝐴𝜑
51, 2, 3wral 2435 . . 3 wff 𝑥𝐴 𝜑
62cv 1334 . . . . 5 class 𝑥
76, 3wcel 2128 . . . 4 wff 𝑥𝐴
87, 2wex 1472 . . 3 wff 𝑥 𝑥𝐴
95, 8wa 103 . 2 wff (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴)
104, 9wb 104 1 wff (∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
Colors of variables: wff set class
This definition is referenced by:  alsconv  13690  alsc1d  13693  alsc2d  13694
  Copyright terms: Public domain W3C validator