Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-if | Structured version Visualization version GIF version |
Description: Define the conditional
operator. Read if(𝜑, 𝐴, 𝐵) as "if
𝜑 then 𝐴 else 𝐵."
See iftrue 4125 and iffalse 4128 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 4172 for the main part of the weak deduction theorem, elimhyp 4179 to eliminate a hypothesis, and keephyp 4185 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.) |
Ref | Expression |
---|---|
df-if | ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | cA | . . 3 class 𝐴 | |
3 | cB | . . 3 class 𝐵 | |
4 | 1, 2, 3 | cif 4119 | . 2 class if(𝜑, 𝐴, 𝐵) |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1522 | . . . . . 6 class 𝑥 |
7 | 6, 2 | wcel 2030 | . . . . 5 wff 𝑥 ∈ 𝐴 |
8 | 7, 1 | wa 383 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 6, 3 | wcel 2030 | . . . . 5 wff 𝑥 ∈ 𝐵 |
10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
11 | 9, 10 | wa 383 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
12 | 8, 11 | wo 382 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
13 | 12, 5 | cab 2637 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
14 | 4, 13 | wceq 1523 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfif2 4121 dfif6 4122 iffalse 4128 rabsnifsb 4289 bj-dfifc2 32689 |
Copyright terms: Public domain | W3C validator |