Definition df-if 4529

Description: Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4534 and iffalse 4537 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 4586. (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 4528	. 2 class if(𝜑, 𝐴, 𝐵)
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1541	. . . . . 6 class 𝑥
7	6, 2	wcel 2107	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 397	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	6, 3	wcel 2107	. . . . 5 wff 𝑥 ∈ 𝐵
10	1	wn 3	. . . . 5 wff ¬ 𝜑
11	9, 10	wa 397	. . . 4 wff (𝑥 ∈ 𝐵 ∧ ¬ 𝜑)
12	8, 11	wo 846	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))
13	12, 5	cab 2710	. 2 class {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
14	4, 13	wceq 1542	1 wff if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}

This definition is referenced by:  dfif2  4530  dfif6  4531  iffalse  4537  rabsnifsb  4726  bj-df-ifc  35446