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

Definition df-if 3663
 Description: Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." 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, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. 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 if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}
Distinct variable groups:   φ,x   x,A   x,B

Detailed syntax breakdown of Definition df-if
StepHypRef Expression
1 wph . . 3 wff φ
2 cA . . 3 class A
3 cB . . 3 class B
41, 2, 3cif 3662 . 2 class if(φ, A, B)
5 vx . . . . . . 7 setvar x
65cv 1641 . . . . . 6 class x
76, 2wcel 1710 . . . . 5 wff x A
87, 1wa 358 . . . 4 wff (x A φ)
96, 3wcel 1710 . . . . 5 wff x B
101wn 3 . . . . 5 wff ¬ φ
119, 10wa 358 . . . 4 wff (x B ¬ φ)
128, 11wo 357 . . 3 wff ((x A φ) (x B ¬ φ))
1312, 5cab 2339 . 2 class {x ((x A φ) (x B ¬ φ))}
144, 13wceq 1642 1 wff if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}
 Colors of variables: wff setvar class This definition is referenced by:  dfif2  3664  dfif6  3665  iffalse  3669
 Copyright terms: Public domain W3C validator