Definition df-if 4460

Description: Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4465 and iffalse 4468 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 4517. (Contributed by NM, 15-May-1999.)

Assertion

Ref	Expression
df-if	⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-if

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	cif 4459	. 2 class if(𝜑, 𝐴, 𝐵)
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1538	. . . . . 6 class 𝑥
7	6, 2	wcel 2106	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 396	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	6, 3	wcel 2106	. . . . 5 wff 𝑥 ∈ 𝐵
10	1	wn 3	. . . . 5 wff ¬ 𝜑
11	9, 10	wa 396	. . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)
12	8, 11	wo 844	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))
13	12, 5	cab 2715	. 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
14	4, 13	wceq 1539	1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

This definition is referenced by:  dfif2  4461  dfif6  4462  iffalse  4468  rabsnifsb  4658  bj-df-ifc  34769