Definition df-if 4280

Description: Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4285 and iffalse 4288 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 4335. (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 4279	. 2 class if(𝜑, 𝐴, 𝐵)
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1636	. . . . . 6 class 𝑥
7	6, 2	wcel 2156	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 384	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	6, 3	wcel 2156	. . . . 5 wff 𝑥 ∈ 𝐵
10	1	wn 3	. . . . 5 wff ¬ 𝜑
11	9, 10	wa 384	. . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)
12	8, 11	wo 865	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))
13	12, 5	cab 2792	. 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
14	4, 13	wceq 1637	1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

This definition is referenced by:  dfif2  4281  dfif6  4282  iffalse  4288  rabsnifsb  4448  bj-dfifc2  32874