NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-mo Unicode version

Definition df-mo 2209
Description: Define "there exists at most one such that ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2235. For other possible definitions see mo2 2233 and mo4 2237. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
df-mo

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2wmo 2205 . 2
41, 2wex 1541 . . 3
51, 2weu 2204 . . 3
64, 5wi 4 . 2
73, 6wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  nfmo1  2215  nfmod2  2217  sb8mo  2223  mo2  2233  mobid  2238  cbvmo  2241  exmoeu  2246  moabs  2248  exmo  2249  2euex  2276  rmo5  2827  moeq  3012  dff3  5420
  Copyright terms: Public domain W3C validator