Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-if | Unicode version |
Description: Define the conditional
operator. Read as "if
then
else ." See iftrue 3479 and iffalse 3482 for its
values. In mathematical literature, this operator is rarely defined
formally but is implicit in informal definitions such as "let
f(x)=0 if
x=0 and 1/x otherwise."
In the absence of excluded middle, this will tend to be useful where is decidable (in the sense of df-dc 820). (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
df-if |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | cA | . . 3 | |
3 | cB | . . 3 | |
4 | 1, 2, 3 | cif 3474 | . 2 |
5 | vx | . . . . . . 7 | |
6 | 5 | cv 1330 | . . . . . 6 |
7 | 6, 2 | wcel 1480 | . . . . 5 |
8 | 7, 1 | wa 103 | . . . 4 |
9 | 6, 3 | wcel 1480 | . . . . 5 |
10 | 1 | wn 3 | . . . . 5 |
11 | 9, 10 | wa 103 | . . . 4 |
12 | 8, 11 | wo 697 | . . 3 |
13 | 12, 5 | cab 2125 | . 2 |
14 | 4, 13 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfif6 3476 iftrue 3479 iffalse 3482 ifbi 3492 nfifd 3499 ifmdc 3509 |
Copyright terms: Public domain | W3C validator |