MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-if Unicode version

Definition df-if 3942
Description: Define the conditional operator. Read as "if then else ." See iftrue 3947 and iffalse 3950 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 older versions of this database, this operator was denoted "ded" and called the "deduction class.")

An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, is a class variable in the hypothesis and is a class (usually a constant) that makes the hypothesis true when it is substituted for . See dedth 3993 for the main part of the weak deduction theorem, elimhyp 4000 to eliminate a hypothesis, and keephyp 4006 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem. (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 3941 . 2
5 vx . . . . . . 7
65cv 1394 . . . . . 6
76, 2wcel 1818 . . . . 5
87, 1wa 369 . . . 4
96, 3wcel 1818 . . . . 5
101wn 3 . . . . 5
119, 10wa 369 . . . 4
128, 11wo 368 . . 3
1312, 5cab 2442 . 2
144, 13wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfif2  3943  dfif6  3944  iffalse  3950  rabsnifsb  4098  bj-dfifc2  34164
  Copyright terms: Public domain W3C validator