NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-if Unicode version

Definition df-if 3663
Description: Define the conditional operator. Read as "if then else ." See iftrue 3668 and iffalse 3669 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 3703 for the main part of the weak deduction theorem, elimhyp 3710 to eliminate a hypothesis, and keephyp 3716 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 3662 . 2
5 vx . . . . . . 7
65cv 1641 . . . . . 6
76, 2wcel 1710 . . . . 5
87, 1wa 358 . . . 4
96, 3wcel 1710 . . . . 5
101wn 3 . . . . 5
119, 10wa 358 . . . 4
128, 11wo 357 . . 3
1312, 5cab 2339 . 2
144, 13wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  dfif2  3664  dfif6  3665  iffalse  3669
  Copyright terms: Public domain W3C validator