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 4471 and iffalse 4474 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 4521. (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 4465 | . 2 class if(𝜑, 𝐴, 𝐵) |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1527 | . . . . . 6 class 𝑥 |
7 | 6, 2 | wcel 2105 | . . . . 5 wff 𝑥 ∈ 𝐴 |
8 | 7, 1 | wa 396 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 6, 3 | wcel 2105 | . . . . 5 wff 𝑥 ∈ 𝐵 |
10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
11 | 9, 10 | wa 396 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
12 | 8, 11 | wo 841 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
13 | 12, 5 | cab 2799 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
14 | 4, 13 | wceq 1528 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfif2 4467 dfif6 4468 iffalse 4474 rabsnifsb 4652 bj-df-ifc 33811 |
Copyright terms: Public domain | W3C validator |