Definition df-if 3520

Description: Define the conditional operator. Read if ( ph , A , B ) as "if ph then A else B". See iftrue 3524 and iffalse 3527 for its values. In 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."

In the absence of excluded middle, this will tend to be useful where ph is decidable (in the sense of df-dc 825). (Contributed by NM, 15-May-1999.)

Assertion

Ref	Expression
df-if	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }

Distinct variable groups:   ph, x   x, A   x, B

Detailed syntax breakdown of Definition df-if

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cif 3519	. 2 class if ( ph , A , B )
5		vx	. . . . . . 7 setvar x
6	5	cv 1342	. . . . . 6 class x
7	6, 2	wcel 2136	. . . . 5 wff x e. A
8	7, 1	wa 103	. . . 4 wff ( x e. A /\ ph )
9	6, 3	wcel 2136	. . . . 5 wff x e. B
10	1	wn 3	. . . . 5 wff -. ph
11	9, 10	wa 103	. . . 4 wff ( x e. B /\ -. ph )
12	8, 11	wo 698	. . 3 wff ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) )
13	12, 5	cab 2151	. 2 class { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
14	4, 13	wceq 1343	1 wff if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }

This definition is referenced by:  dfif6  3521  iftrue  3524  iffalse  3527  ifbi  3539  nfifd  3546  ifmdc  3557  if0ab  13647