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 3449 and iffalse 3452 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 805). (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 3444 | . 2 |
5 | vx | . . . . . . 7 | |
6 | 5 | cv 1315 | . . . . . 6 |
7 | 6, 2 | wcel 1465 | . . . . 5 |
8 | 7, 1 | wa 103 | . . . 4 |
9 | 6, 3 | wcel 1465 | . . . . 5 |
10 | 1 | wn 3 | . . . . 5 |
11 | 9, 10 | wa 103 | . . . 4 |
12 | 8, 11 | wo 682 | . . 3 |
13 | 12, 5 | cab 2103 | . 2 |
14 | 4, 13 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfif6 3446 iftrue 3449 iffalse 3452 ifbi 3462 nfifd 3469 ifmdc 3479 |
Copyright terms: Public domain | W3C validator |