Definition df-if

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

	Ref	Expression
Assertion	df-if	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	cif	$$classif\left(\phi ,A,B\right)$$
4		vx	$$setvarx$$
5	4	cv	$$setvarx$$
6	5 1	wcel	$$wffx\in A$$
7	6 0	wa	$$wff\left(x\in A\wedge \phi \right)$$
8	5 2	wcel	$$wffx\in B$$
9	0	wn	$$wff\neg \phi$$
10	8 9	wa	$$wff\left(x\in B\wedge \neg \phi \right)$$
11	7 10	wo	$$wff\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)$$
12	11 4	cab	$$class\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
13	3 12	wceq	$$wffif\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$