![]() |
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 4527 and iffalse 4530 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 4579. (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 4521 | . 2 class if(𝜑, 𝐴, 𝐵) |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1532 | . . . . . 6 class 𝑥 |
7 | 6, 2 | wcel 2098 | . . . . 5 wff 𝑥 ∈ 𝐴 |
8 | 7, 1 | wa 395 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 6, 3 | wcel 2098 | . . . . 5 wff 𝑥 ∈ 𝐵 |
10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
11 | 9, 10 | wa 395 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
12 | 8, 11 | wo 844 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
13 | 12, 5 | cab 2701 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
14 | 4, 13 | wceq 1533 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfif2 4523 dfif6 4524 iffalse 4530 rabsnifsb 4719 bj-df-ifc 35948 |
Copyright terms: Public domain | W3C validator |