Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-if Unicode version

Definition df-if 3359
 Description: Define the conditional operator. Read as "if then else ." See iftrue 3363 and iffalse 3366 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 754). (Contributed by NM, 15-May-1999.)
Assertion
Ref Expression
df-if
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Definition df-if
StepHypRef Expression
1 wph . . 3
2 cA . . 3
3 cB . . 3
41, 2, 3cif 3358 . 2
5 vx . . . . . . 7
65cv 1258 . . . . . 6
76, 2wcel 1409 . . . . 5
87, 1wa 101 . . . 4
96, 3wcel 1409 . . . . 5
101wn 3 . . . . 5
119, 10wa 101 . . . 4
128, 11wo 639 . . 3
1312, 5cab 2042 . 2
144, 13wceq 1259 1
 Colors of variables: wff set class This definition is referenced by:  dfif6  3360  iftrue  3363  iffalse  3366  ifbi  3375  nfifd  3382
 Copyright terms: Public domain W3C validator