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

Definition df-if 3826
 Description: Define the conditional operator. Read as "if then else ." See iftrue 3831 and iffalse 3833 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 3874 for the main part of the weak deduction theorem, elimhyp 3881 to eliminate a hypothesis, and keephyp 3887 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 3825 . 2
5 vx . . . . . . 7
65cv 1669 . . . . . 6
76, 2wcel 1732 . . . . 5
87, 1wa 360 . . . 4
96, 3wcel 1732 . . . . 5
101wn 3 . . . . 5
119, 10wa 360 . . . 4
128, 11wo 359 . . 3
1312, 5cab 2475 . 2
144, 13wceq 1670 1
 Colors of variables: wff set class This definition is referenced by:  dfif2  3827  dfif6  3828  iffalse  3833
 Copyright terms: Public domain W3C validator