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

Definition df-alsc 46164
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 46162 . 2 wff ∀!𝑥𝐴𝜑
51, 2, 3wral 3061 . . 3 wff 𝑥𝐴 𝜑
62cv 1542 . . . . 5 class 𝑥
76, 3wcel 2110 . . . 4 wff 𝑥𝐴
87, 2wex 1787 . . 3 wff 𝑥 𝑥𝐴
95, 8wa 399 . 2 wff (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴)
104, 9wb 209 1 wff (∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  alsconv  46165  alsc1d  46168  alsc2d  46169
  Copyright terms: Public domain W3C validator