Theorem iffalse 3634

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)

Assertion

Ref	Expression
iffalse	⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalse

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-if 3625	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 979	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2355	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2286	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716   = wceq 1398   ∈ wcel 2205  {cab 2220  ifcif 3624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  iffalsei  3635  iffalsed  3636  ifnefalse  3637  ifsbdc  3639  ifcldadc  3656  ifeq1dadc  3657  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  ifcldcd  3664  ifnotdc  3665  2if2dc  3666  ifandc  3667  ifordc  3668  ifnetruedc  3670  pw2f1odclem  7100  fidifsnen  7138  nnnninf  7430  uzin  9908  modifeq2int  10775  seqf1oglem1  10908  seqf1oglem2  10909  bcval  11139  bcval3  11141  swrdccat  11455  pfxccat3a  11458  swrdccat3b  11460  sumrbdclem  12092  fsum3cvg  12093  summodclem2a  12096  sumsplitdc  12147  prodrbdclem  12286  fproddccvg  12287  prodssdc  12304  flodddiv4  12651  gcdn0val  12686  dfgcd2  12739  lcmn0val  12792  pcgcd  13056  pcmptcl  13069  pcmpt  13070  pcmpt2  13071  pcprod  13073  fldivp1  13075  unct  13281  lgsneg  16027  lgsdilem  16030  lgsdir2  16036  lgsdir  16038  lgsdi  16040  lgsne0  16041  gausslemma2dlem1a  16061  2lgslem1c  16093  2lgs  16107