# Metamath Proof Explorer

## 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 ¬{\phi }\right)\right)\right\}$

### Detailed syntax breakdown

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