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

Definition df-if 3326
Description: Define the conditional operator. Read  if ,  , as "if then else ." See iftrue 3330 and iffalse 3333 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 742). (Contributed by NM, 15-May-1999.)

Assertion
Ref Expression
df-if  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 3325 . 2  if ,  ,
5 vx . . . . . . 7  setvar
65cv 1241 . . . . . 6
76, 2wcel 1390 . . . . 5
87, 1wa 97 . . . 4
96, 3wcel 1390 . . . . 5
101wn 3 . . . . 5
119, 10wa 97 . . . 4
128, 11wo 628 . . 3
1312, 5cab 2023 . 2  {  |  }
144, 13wceq 1242 1  if ,  ,  {  |  }
Colors of variables: wff set class
This definition is referenced by:  dfif6  3327  iftrue  3330  iffalse  3333  ifbi  3342  nfifd  3349
  Copyright terms: Public domain W3C validator