Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-iota | Structured version Visualization version GIF version |
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 6444);
otherwise, it evaluates to the empty set (see iotanul 6451). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based 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 riotacl2 7303 (or iotacl 6459 for unbounded iota), as demonstrated in the proof of supub 9308. This can be easier than applying riotasbc 7305 or 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, 30-Jun-2011.) |
Ref | Expression |
---|---|
df-iota | ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | cio 6423 | . 2 class (℩𝑥𝜑) |
4 | 1, 2 | cab 2713 | . . . . 5 class {𝑥 ∣ 𝜑} |
5 | vy | . . . . . . 7 setvar 𝑦 | |
6 | 5 | cv 1539 | . . . . . 6 class 𝑦 |
7 | 6 | csn 4572 | . . . . 5 class {𝑦} |
8 | 4, 7 | wceq 1540 | . . . 4 wff {𝑥 ∣ 𝜑} = {𝑦} |
9 | 8, 5 | cab 2713 | . . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
10 | 9 | cuni 4851 | . 2 class ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
11 | 3, 10 | wceq 1540 | 1 wff (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
Colors of variables: wff setvar class |
This definition is referenced by: dfiota2 6426 cbviotavw 6433 iotaeq 6438 iotabi 6439 iotaval2 6441 iotanul2 6443 dffv4 6816 dfiota3 34316 sn-iotalemcor 40441 reuabaiotaiota 44919 |
Copyright terms: Public domain | W3C validator |