| 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 4531 and iffalse 4534 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 4584. (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 4525 | . 2 class if(𝜑, 𝐴, 𝐵) |
| 5 | vx | . . . . . . 7 setvar 𝑥 | |
| 6 | 5 | cv 1539 | . . . . . 6 class 𝑥 |
| 7 | 6, 2 | wcel 2108 | . . . . 5 wff 𝑥 ∈ 𝐴 |
| 8 | 7, 1 | wa 395 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
| 9 | 6, 3 | wcel 2108 | . . . . 5 wff 𝑥 ∈ 𝐵 |
| 10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
| 11 | 9, 10 | wa 395 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
| 12 | 8, 11 | wo 848 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
| 13 | 12, 5 | cab 2714 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
| 14 | 4, 13 | wceq 1540 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfif2 4527 dfif6 4528 iffalse 4534 rabsnifsb 4722 bj-df-ifc 36581 |
| Copyright terms: Public domain | W3C validator |