Definition df-if 4525

Description: Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4530 and iffalse 4533 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 4582. (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 4524	. 2 class if(𝜑, 𝐴, 𝐵)
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1533	. . . . . 6 class 𝑥
7	6, 2	wcel 2099	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 395	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	6, 3	wcel 2099	. . . . 5 wff 𝑥 ∈ 𝐵
10	1	wn 3	. . . . 5 wff ¬ 𝜑
11	9, 10	wa 395	. . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)
12	8, 11	wo 846	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))
13	12, 5	cab 2705	. 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
14	4, 13	wceq 1534	1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

This definition is referenced by:  dfif2  4526  dfif6  4527  iffalse  4533  rabsnifsb  4722  bj-df-ifc  36050