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

Definition df-iota 4339
Description: Define Russell's definition description binder, which can be read as "the unique such that ," where ordinarily contains as a free variable. Our definition is meaningful only when there is exactly one such that is true (see iotaval 4350); otherwise, it evaluates to the empty set (see iotanul 4354). Russell used the inverted iota symbol to represent the binder. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-iota
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Detailed syntax breakdown of Definition df-iota
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2cio 4337 . 2
41, 2cab 2339 . . . . 5
5 vy . . . . . . 7
65cv 1641 . . . . . 6
76csn 3737 . . . . 5
84, 7wceq 1642 . . . 4
98, 5cab 2339 . . 3
109cuni 3891 . 2
113, 10wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  dfiota2  4340  iotaeq  4347  iotabi  4348  fvco2  5382
  Copyright terms: Public domain W3C validator