Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > dfiota  Structured version GIF version 
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 4821);
otherwise, it evaluates to the empty set (see iotanul 4825). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iotabased definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use iotacl 4833 (for unbounded iota). This can be easier than applying a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30Jun2011.) 
Ref  Expression 

dfiota  ⊢ (℩xφ) = ∪ {y ∣ {x ∣ φ} = {y}} 
Step  Hyp  Ref  Expression 

1  wph  . . 3 wff φ  
2  vx  . . 3 setvar x  
3  1, 2  cio 4808  . 2 class (℩xφ) 
4  1, 2  cab 2023  . . . . 5 class {x ∣ φ} 
5  vy  . . . . . . 7 setvar y  
6  5  cv 1241  . . . . . 6 class y 
7  6  csn 3367  . . . . 5 class {y} 
8  4, 7  wceq 1242  . . . 4 wff {x ∣ φ} = {y} 
9  8, 5  cab 2023  . . 3 class {y ∣ {x ∣ φ} = {y}} 
10  9  cuni 3571  . 2 class ∪ {y ∣ {x ∣ φ} = {y}} 
11  3, 10  wceq 1242  1 wff (℩xφ) = ∪ {y ∣ {x ∣ φ} = {y}} 
Colors of variables: wff set class 
This definition is referenced by: dfiota2 4811 iotaeq 4818 iotabi 4819 iotass 4827 dffv4g 5118 nfvres 5149 
Copyright terms: Public domain  W3C validator 