Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-if | GIF version |
Description: Define the conditional
operator. Read if(𝜑, 𝐴, 𝐵) as "if
𝜑 then 𝐴 else 𝐵".
See iftrue 3530 and iffalse 3533 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 the absence of excluded middle, this will tend to be useful where 𝜑 is decidable (in the sense of df-dc 830). (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 3525 | . 2 class if(𝜑, 𝐴, 𝐵) |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1347 | . . . . . 6 class 𝑥 |
7 | 6, 2 | wcel 2141 | . . . . 5 wff 𝑥 ∈ 𝐴 |
8 | 7, 1 | wa 103 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 6, 3 | wcel 2141 | . . . . 5 wff 𝑥 ∈ 𝐵 |
10 | 1 | wn 3 | . . . . 5 wff ¬ 𝜑 |
11 | 9, 10 | wa 103 | . . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑) |
12 | 8, 11 | wo 703 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)) |
13 | 12, 5 | cab 2156 | . 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
14 | 4, 13 | wceq 1348 | 1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
Colors of variables: wff set class |
This definition is referenced by: dfif6 3527 iftrue 3530 iffalse 3533 ifbi 3545 nfifd 3552 ifmdc 3563 if0ab 13762 |
Copyright terms: Public domain | W3C validator |