Description: Definition of the conditional operator for classes. The expression if ( ph , A , B ) is read "if ph then A else B ". See iftrue and iffalse 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 . (Contributed by NM, 15-May-1999)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-if | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | ⊢ 𝜑 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | cB | ⊢ 𝐵 | |
| 3 | 0 1 2 | cif | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) |
| 4 | vx | ⊢ 𝑥 | |
| 5 | 4 | cv | ⊢ 𝑥 |
| 6 | 5 1 | wcel | ⊢ 𝑥 ∈ 𝐴 |
| 7 | 6 0 | wa | ⊢ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) |
| 8 | 5 2 | wcel | ⊢ 𝑥 ∈ 𝐵 |
| 9 | 0 | wn | ⊢ ¬ 𝜑 |
| 10 | 8 9 | wa | ⊢ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) |
| 11 | 7 10 | wo | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) |
| 12 | 11 4 | cab | ⊢ { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } |
| 13 | 3 12 | wceq | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } |