Definition df-if 2359

Description: Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." See iftrue 2363 and iffalse 2364 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 older versions of this database, this operator was denoted "ded" and called the "deduction class.")

An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. See dedth 2380 for the main part of the weak deduction theorem, elimhyp 2387 to eliminate a hypothesis, and keephyp 2393 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem.

Assertion

Ref	Expression
df-if	⊢ if(φ, A, B) = {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}

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

Detailed syntax breakdown of Definition df-if

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cif 2358	. 2 class if(φ, A, B)
5		vx	. . . . . . 7 set x
6	5	cv 954	. . . . . 6 class x
7	6, 2	wcel 957	. . . . 5 wff x ∈ A
8	7, 1	wa 223	. . . 4 wff (x ∈ A ⋀ φ)
9	6, 3	wcel 957	. . . . 5 wff x ∈ B
10	1	wn 2	. . . . 5 wff ¬ φ
11	9, 10	wa 223	. . . 4 wff (x ∈ B ⋀ ¬ φ)
12	8, 11	wo 222	. . 3 wff ((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))
13	12, 5	cab 1462	. 2 class {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}
14	4, 13	wceq 955	1 wff if(φ, A, B) = {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}

This definition is referenced by:  dfif2 2360  ifeq1 2361  ifeq2 2362  iftrue 2363  iffalse 2364  hbif 2370

Copyright terms: Public domain