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 3336 and iffalse 3339 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 743). (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 3331 | . 2 |
5 | vx | . . . . . . 7 | |
6 | 5 | cv 1242 | . . . . . 6 |
7 | 6, 2 | wcel 1393 | . . . . 5 |
8 | 7, 1 | wa 97 | . . . 4 |
9 | 6, 3 | wcel 1393 | . . . . 5 |
10 | 1 | wn 3 | . . . . 5 |
11 | 9, 10 | wa 97 | . . . 4 |
12 | 8, 11 | wo 629 | . . 3 |
13 | 12, 5 | cab 2026 | . 2 |
14 | 4, 13 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfif6 3333 iftrue 3336 iffalse 3339 ifbi 3348 nfifd 3355 |
Copyright terms: Public domain | W3C validator |