![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-if | Structured version Visualization version GIF version |
Description: Definition of the
conditional operator for classes. The expression
if(𝜑,
𝐴, 𝐵) is read "if 𝜑 then
𝐴
else 𝐵". See
iftrue 4381 and iffalse 4384 for its values. In the 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".
An important use for us is in conjunction with the weak deduction theorem, which is described in the next section, beginning at dedth 4431. (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 4375 | . 2 class if(𝜑, 𝐴, 𝐵) |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1519 | . . . . . 6 class 𝑥 |
7 | 6, 2 | wcel 2079 | . . . . 5 wff 𝑥 ∈ 𝐴 |
8 | 7, 1 | wa 396 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 6, 3 | wcel 2079 | . . . . 5 wff 𝑥 ∈ 𝐵 |
10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
11 | 9, 10 | wa 396 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
12 | 8, 11 | wo 842 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
13 | 12, 5 | cab 2773 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
14 | 4, 13 | wceq 1520 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfif2 4377 dfif6 4378 iffalse 4384 rabsnifsb 4559 bj-dfifc2 33463 |
Copyright terms: Public domain | W3C validator |