Definition df-if 4493

Description: Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4498 and iffalse 4501 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 4551. (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 4492	. 2 class if(𝜑, 𝐴, 𝐵)
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1569	. . . . . 6 class 𝑥
7	6, 2	wcel 2146	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	6, 3	wcel 2146	. . . . 5 wff 𝑥 ∈ 𝐵
10	1	wn 3	. . . . 5 wff ¬ 𝜑
11	9, 10	wa 401	. . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)
12	8, 11	wo 861	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))
13	12, 5	cab 2744	. 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
14	4, 13	wceq 1570	1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

This definition is used by:  dfif2  4494  dfif6  4495  iffalse  4501  rabsnifsb  4693  bj-df-ifc  37206