HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-if 2352
Description: Define the conditional operator. Read if(ph, A, B) as "if ph then A else B." See iftrue 2356 and iffalse 2357 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 2373 for the main part of the weak deduction theorem, elimhyp 2380 to eliminate a hypothesis, and keephyp 2386 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem.

Assertion
Ref Expression
df-if |- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
Distinct variable groups:   ph,x   x,A   x,B
Detailed syntax breakdown of Definition df-if
StepHypRef Expression
1 wph . . 3 wff ph
2 cA . . 3 class A
3 cB . . 3 class B
41, 2, 3cif 2351 . 2 class if(ph, A, B)
5 vx . . . . . . 7 set x
65cv 952 . . . . . 6 class x
76, 2wcel 955 . . . . 5 wff x e. A
87, 1wa 223 . . . 4 wff (x e. A /\ ph)
96, 3wcel 955 . . . . 5 wff x e. B
101wn 2 . . . . 5 wff -. ph
119, 10wa 223 . . . 4 wff (x e. B /\ -. ph)
128, 11wo 222 . . 3 wff ((x e. A /\ ph) \/ (x e. B /\ -. ph))
1312, 5cab 1456 . 2 class {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
144, 13wceq 953 1 wff if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
Colors of variables: wff set class
This definition is referenced by:  dfif2 2353  ifeq1 2354  ifeq2 2355  iftrue 2356  iffalse 2357  hbif 2363
Copyright terms: Public domain