Theorem iffalse 4359

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		dedlemb 1027	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
2	1	abbi2dv 2903	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
3		df-if 4351	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
4	2, 3	syl6reqr 2834	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2050  {cab 2759  ifcif 4350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-if 4351

This theorem is referenced by:  iffalsei  4360  iffalsed  4361  ifnefalse  4362  ifsb  4363  ifbi  4371  ifeq1da  4380  ifeq12da  4382  ifclda  4384  ifeqda  4385  elimif  4386  ifbothda  4387  ifid  4389  ifnot  4400  ifan  4401  ifor  4402  2if2  4403  ifcomnan  4404  elimhyp  4413  elimhyp2v  4414  elimhyp3v  4415  elimhyp4v  4416  elimdhyp  4418  keephyp2v  4420  keephyp3v  4421  dfopif  4674  opprc  4700  somin1  5833  elimdelov  7066  ovif12  7069  oevn0  7942  pw2f1olem  8417  unxpdomlem2  8518  unxpdomlem3  8519  infsupprpr  8763  oi0  8787  wemaplem2  8806  ixpiunwdom  8850  cantnfp1lem3  8937  cantnflem1  8946  dfac12lem2  9364  fin23lem14  9553  axcc2lem  9656  ttukeylem5  9733  uzin  12092  xrmax1  12385  xrmax2  12386  xrmin1  12387  xrmin2  12388  max1ALT  12396  ifle  12407  xmulneg1  12478  modifeq2int  13116  seqf1olem1  13224  seqf1olem2  13225  bcval3  13481  swrdccat  13938  swrdccatOLD  13939  pfxccat3a  13942  swrdccat3aOLD  13943  swrdccat3b  13945  swrdccat3bOLD  13946  repswswrd  14003  cshword  14013  ccatco  14059  sumrblem  14928  fsumcvg  14929  summolem2a  14932  sumss  14941  fsumcvg2  14944  sumsplit  14983  prodeq2ii  15127  prodrblem  15143  fprodcvg  15144  prodmolem2a  15148  zprod  15151  prodss  15161  ruclem2  15445  ruclem3  15446  flodddiv4  15624  sadadd2lem2  15659  sadcp1  15664  sadcaddlem  15666  gcdn0val  15707  dfgcd2  15750  lcmn0val  15795  lcmfn0val  15823  pcgcd  16070  pcmptcl  16083  pcmpt  16084  pcmpt2  16085  pcprod  16087  fldivp1  16089  prmreclem2  16109  prmreclem4  16111  vdwlem6  16178  prmop1  16230  fvprmselelfz  16236  fvprmselgcd1  16237  ressval2  16409  xpsaddlem  16704  xpsvsca  16708  mreexexd  16777  setcepi  17206  pmtrmvd  18345  mvrf1  19919  mplcoe3  19960  mplmon2  19986  psrbagsn  19988  evlslem1  20008  obselocv  20574  dmatmul  20810  1mavmul  20861  mulmarep1gsum2  20887  1marepvmarrepid  20888  mdetdiag  20912  mdetrsca2  20917  mdetrlin2  20920  mdetunilem5  20929  mdetunilem7  20931  mdetunilem8  20932  mdetunilem9  20933  mndifsplit  20949  maducoeval2  20953  madugsum  20956  madurid  20957  smadiadetglem2  20985  1elcpmat  21027  decpmatid  21082  ptpjpre1  21883  ptbasfi  21893  isfcls  22321  ptcmplem2  22365  ptcmplem3  22366  dscmet  22885  dscopn  22886  icccmplem2  23134  cnmpopc  23235  iccpnfcnv  23251  xrhmeo  23253  pcoval2  23323  pcopt  23329  pcopt2  23330  pcoass  23331  pcorevlem  23333  i1f1lem  23993  itg1addlem2  24001  itg1addlem3  24002  i1fres  24009  itg1climres  24018  mbfi1fseqlem4  24022  mbfi1fseqlem5  24023  itg2const2  24045  itg2seq  24046  itg2uba  24047  itg2splitlem  24052  itg2split  24053  itg2monolem1  24054  itg2gt0  24064  itg2cnlem1  24065  itg2cnlem2  24066  iblss  24108  iblss2  24109  itgle  24113  itgss  24115  ibladdlem  24123  itgaddlem1  24126  iblabslem  24131  iblabs  24132  iblabsr  24133  iblmulc2  24134  bddmulibl  24142  ditgneg  24158  elply2  24489  coeeq2  24535  dgrle  24536  coe1termlem  24551  logcnlem3  24928  igamgam  25328  isppw  25393  isnsqf  25414  mule1  25427  sqff1o  25461  chtublem  25489  dchrelbasd  25517  bposlem1  25562  bposlem3  25564  bposlem5  25566  bposlem6  25567  lgsneg  25599  lgsdilem  25602  lgsdir2  25608  lgsdir  25610  lgsdi  25612  lgsne0  25613  gausslemma2dlem1a  25643  2lgslem1c  25671  2lgs  25685  dchrvmasum2if  25775  ostth2lem4  25914  axlowdimlem15  26445  elimifd  30066  elim2if  30067  ifeq3da  30069  imadifxp  30117  resvval2  30578  pmtridf1o  30694  xrge0iifcnv  30817  indval2  30914  ddeval0  31136  eulerpartlemb  31268  plymulx0  31460  signsw0glem  31466  signswmnd  31470  dfrdg2  32558  dfrdg3  32559  noprefixmo  32720  nosupno  32721  nosupdm  32722  nosupbday  32723  nosupfv  32724  nosupres  32725  nosupbnd1lem1  32726  unisnif  32904  dfrdg4  32930  bj-xpima1sn  33761  finxpreclem2  34109  finxpreclem5  34114  matunitlindflem1  34326  poimirlem15  34345  poimirlem23  34353  mbfposadd  34377  itg2addnclem  34381  itg2addnclem3  34383  itg2gt0cn  34385  ibladdnclem  34386  itgaddnclem1  34388  iblabsnclem  34393  iblabsnc  34394  iblmulc2nc  34395  bddiblnc  34400  ftc1anclem5  34409  ftc1anclem7  34411  ftc1anclem8  34412  ftc1anc  34413  areacirclem5  34424  areacirc  34425  heiborlem4  34531  ac6s6  34891  riotaclbgBAD  35532  cdleme27a  36945  cdleme31sn2  36967  dihvalc  37811  mapdhval2  38304  hdmap1val2  38378  dffltz  38675  pw2f1ocnv  39027  aomclem5  39051  arearect  39215  areaquad  39216  fincygsubgodd  40044  upbdrech2  41002  lptioo2  41341  lptioo1  41342  limsupmnfuzlem  41436  limsupre3uzlem  41445  limsup10exlem  41482  coskpi2  41575  cosknegpi  41578  icccncfext  41598  cncfiooicclem1  41604  cncfiooiccre  41606  ioodvbdlimc1lem2  41645  ioodvbdlimc2lem  41647  itgioocnicc  41690  iblcncfioo  41691  volico  41697  sublevolico  41698  voliooico  41706  voliccico  41713  dirkerper  41810  dirkertrigeq  41815  dirkercncflem2  41818  fourierdlem10  41831  fourierdlem32  41853  fourierdlem33  41854  fourierdlem37  41858  fourierdlem62  41882  fourierdlem73  41893  fourierdlem74  41894  fourierdlem75  41895  fourierdlem79  41899  fourierdlem81  41901  fourierdlem82  41902  fourierdlem93  41913  fourierdlem97  41917  fourierdlem101  41921  fourierdlem103  41923  fourierdlem104  41924  sqwvfoura  41942  sqwvfourb  41943  fourierswlem  41944  fouriersw  41945  elaa2lem  41947  etransclem15  41963  etransclem19  41967  etransclem23  41971  etransclem24  41972  etransclem25  41973  ioorrnopnxrlem  42020  nnfoctbdjlem  42166  isomenndlem  42241  ovn0  42277  hsphoidmvle2  42296  hoidmv1lelem1  42302  hoidmv1lelem2  42303  hoidmv1le  42305  hoidmvlelem2  42307  hoidmvlelem3  42308  ovnhoilem1  42312  hspdifhsp  42327  hoidifhspdmvle  42331  hspmbllem1  42337  hspmbllem2  42338  hspmbl  42340  volico2  42352  ovolval4lem2  42361  ovolval5lem1  42363  afvnfundmuv  42742  ndfatafv2  42814  prproropf1olem4  43034  suppmptcfin  43791  linc1  43845  ifnmfalse  44227