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

Definition df-if 3700
 Description: Define the conditional operator. Read as "if then else ." See iftrue 3705 and iffalse 3706 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 3740 for the main part of the weak deduction theorem, elimhyp 3747 to eliminate a hypothesis, and keephyp 3753 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 3699 . 2
5 vx . . . . . . 7
65cv 1648 . . . . . 6
76, 2wcel 1721 . . . . 5
87, 1wa 359 . . . 4
96, 3wcel 1721 . . . . 5
101wn 3 . . . . 5
119, 10wa 359 . . . 4
128, 11wo 358 . . 3
1312, 5cab 2390 . 2
144, 13wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  dfif2  3701  dfif6  3702  iffalse  3706
 Copyright terms: Public domain W3C validator