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

Definition df-iota 4339
Description: Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x 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 (℩xφ) = {y {x φ} = {y}}
Distinct variable groups:   x,y   φ,y
Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Definition df-iota
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
31, 2cio 4337 . 2 class (℩xφ)
41, 2cab 2339 . . . . 5 class {x φ}
5 vy . . . . . . 7 setvar y
65cv 1641 . . . . . 6 class y
76csn 3737 . . . . 5 class {y}
84, 7wceq 1642 . . . 4 wff {x φ} = {y}
98, 5cab 2339 . . 3 class {y {x φ} = {y}}
109cuni 3891 . 2 class {y {x φ} = {y}}
113, 10wceq 1642 1 wff (℩xφ) = {y {x φ} = {y}}
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