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

Definition df-if 3766
Description: Define the conditional operator. Read as "if then else ." See iftrue 3771 and iffalse 3772 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 3807 for the main part of the weak deduction theorem, elimhyp 3814 to eliminate a hypothesis, and keephyp 3820 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 3765 . 2
5 vx . . . . . . 7
65cv 1653 . . . . . 6
76, 2wcel 1728 . . . . 5
87, 1wa 360 . . . 4
96, 3wcel 1728 . . . . 5
101wn 3 . . . . 5
119, 10wa 360 . . . 4
128, 11wo 359 . . 3
1312, 5cab 2429 . 2
144, 13wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  dfif2  3767  dfif6  3768  iffalse  3772
  Copyright terms: Public domain W3C validator