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 ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		cA	|- A
2		cB	|- B
3	0 1 2	cif	|- if ( ph , A , B )
4		vx	|- x
5	4	cv	|- x
6	5 1	wcel	|- x e. A
7	6 0	wa	|- ( x e. A /\ ph )
8	5 2	wcel	|- x e. B
9	0	wn	|- -. ph
10	8 9	wa	|- ( x e. B /\ -. ph )
11	7 10	wo	|- ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) )
12	11 4	cab	|- { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
13	3 12	wceq	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }