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 4793);
otherwise, it evaluates to the empty set (see iotanul 4797). 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 4805 (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 4780  . 2 class (℩xφ) 
4  1, 2  cab 1999  . . . . 5 class {x ∣ φ} 
5  vy  . . . . . . 7 setvar y  
6  5  cv 1222  . . . . . 6 class y 
7  6  csn 3339  . . . . 5 class {y} 
8  4, 7  wceq 1223  . . . 4 wff {x ∣ φ} = {y} 
9  8, 5  cab 1999  . . 3 class {y ∣ {x ∣ φ} = {y}} 
10  9  cuni 3543  . 2 class ∪ {y ∣ {x ∣ φ} = {y}} 
11  3, 10  wceq 1223  1 wff (℩xφ) = ∪ {y ∣ {x ∣ φ} = {y}} 
Colors of variables: wff set class 
This definition is referenced by: dfiota2 4783 iotaeq 4790 iotabi 4791 iotass 4799 dffv4g 5088 nfvres 5119 
Copyright terms: Public domain  W3C validator 