Theorem iffalse 4557

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 4549	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 1047	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	eqabdv 2878	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2799	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108  {cab 2717  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  iffalsei  4558  iffalsed  4559  ifnefalse  4560  ifsb  4561  ifbi  4570  ifeq1da  4579  ifeq12da  4581  ifclda  4583  ifeqda  4584  elimif  4585  ifbothda  4586  ifid  4588  ifnot  4600  ifan  4601  ifor  4602  2if2  4603  ifcomnan  4604  elimhyp  4613  elimhyp2v  4614  elimhyp3v  4615  elimhyp4v  4616  elimdhyp  4618  keephyp2v  4620  keephyp3v  4621  dfopif  4894  opprc  4920  somin1  6165  elimdelov  7546  brif1  7547  ovif12  7550  oevn0  8571  pw2f1olem  9142  unxpdomlem2  9314  unxpdomlem3  9315  infsupprpr  9573  oi0  9597  wemaplem2  9616  ixpiunwdom  9659  cantnfp1lem3  9749  cantnflem1  9758  dfac12lem2  10214  fin23lem14  10402  axcc2lem  10505  ttukeylem5  10582  uzin  12943  xrmax1  13237  xrmax2  13238  xrmin1  13239  xrmin2  13240  max1ALT  13248  ifle  13259  xmulneg1  13331  modifeq2int  13984  seqf1olem1  14092  seqf1olem2  14093  bcval3  14355  swrdccat  14783  pfxccat3a  14786  swrdccat3b  14788  repswswrd  14832  cshword  14839  ccatco  14884  sumrblem  15759  fsumcvg  15760  summolem2a  15763  sumss  15772  fsumcvg2  15775  sumsplit  15816  prodeq2ii  15959  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  prodss  15995  ruclem2  16280  ruclem3  16281  flodddiv4  16461  sadadd2lem2  16496  sadcp1  16501  sadcaddlem  16503  gcdn0val  16544  dfgcd2  16593  lcmn0val  16642  lcmfn0val  16670  pcgcd  16925  pcmptcl  16938  pcmpt  16939  pcmpt2  16940  pcprod  16942  fldivp1  16944  prmreclem2  16964  prmreclem4  16966  vdwlem6  17033  prmop1  17085  fvprmselelfz  17091  fvprmselgcd1  17092  ressval2  17292  xpsaddlem  17633  xpsvsca  17637  mreexexd  17706  setcepi  18155  pmtrmvd  19498  fincygsubgodd  20156  obselocv  21771  mvrf1  22029  mplcoe3  22079  mplmon2  22108  psrbagsn  22110  evlslem1  22129  mhpsclcl  22174  mhpvarcl  22175  dmatmul  22524  1mavmul  22575  mulmarep1gsum2  22601  1marepvmarrepid  22602  mdetdiag  22626  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  mndifsplit  22663  maducoeval2  22667  madugsum  22670  madurid  22671  smadiadetglem2  22699  1elcpmat  22742  decpmatid  22797  ptpjpre1  23600  ptbasfi  23610  isfcls  24038  ptcmplem2  24082  ptcmplem3  24083  dscmet  24606  dscopn  24607  icccmplem2  24864  cnmpopc  24974  iccpnfcnv  24994  xrhmeo  24996  pcoval2  25068  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  i1f1lem  25743  itg1addlem2  25751  itg1addlem3  25752  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  itg2const2  25796  itg2seq  25797  itg2uba  25798  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  iblss2  25861  itgle  25865  itgss  25867  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  bddmulibl  25894  bddiblnc  25897  ditgneg  25912  elply2  26255  coeeq2  26301  dgrle  26302  coe1termlem  26317  logcnlem3  26704  igamgam  27110  isppw  27175  isnsqf  27196  mule1  27209  sqff1o  27243  chtublem  27273  dchrelbasd  27301  bposlem1  27346  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgsneg  27383  lgsdilem  27386  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsne0  27397  gausslemma2dlem1a  27427  2lgslem1c  27455  2lgs  27469  dchrvmasum2if  27559  ostth2lem4  27698  nosupno  27766  nosupdm  27767  nosupbday  27768  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  noinfno  27781  noinfdm  27782  noinffv  27784  maxs1  27828  maxs2  27829  mins1  27830  mins2  27831  abssnid  28285  abssge0  28287  axlowdimlem15  28989  elimifd  32566  elim2if  32567  ifeq3da  32569  ifnetrue  32570  imadifxp  32623  pmtridf1o  33087  resvval2  33320  xrge0iifcnv  33879  indval2  33978  ddeval0  34199  eulerpartlemb  34333  plymulx0  34524  signsw0glem  34530  signswmnd  34534  dfrdg2  35759  dfrdg3  35760  unisnif  35889  dfrdg4  35915  bj-xpima1sn  36922  finxpreclem2  37356  finxpreclem5  37361  matunitlindflem1  37576  poimirlem15  37595  poimirlem23  37603  mbfposadd  37627  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem5  37672  areacirc  37673  heiborlem4  37774  ac6s6  38132  riotaclbgBAD  38910  cdleme27a  40324  cdleme31sn2  40346  dihvalc  41190  mapdhval2  41683  hdmap1val2  41757  metakunt6  42167  metakunt7  42168  metakunt8  42169  metakunt11  42172  metakunt12  42173  metakunt22  42183  brif2  42217  brif12  42218  fsuppind  42545  dffltz  42589  pw2f1ocnv  42994  aomclem5  43015  arearect  43176  areaquad  43177  safesnsupfidom1o  43379  safesnsupfilb  43380  upbdrech2  45223  lptioo2  45552  lptioo1  45553  limsupmnfuzlem  45647  limsupre3uzlem  45656  limsup10exlem  45693  coskpi2  45787  cosknegpi  45790  icccncfext  45808  cncfiooicclem1  45814  cncfiooiccre  45816  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  itgioocnicc  45898  iblcncfioo  45899  volico  45904  sublevolico  45905  voliooico  45913  voliccico  45920  dirkerper  46017  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem10  46038  fourierdlem32  46060  fourierdlem33  46061  fourierdlem37  46065  fourierdlem62  46089  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem15  46170  etransclem19  46174  etransclem23  46178  etransclem24  46179  etransclem25  46180  ioorrnopnxrlem  46227  nnfoctbdjlem  46376  isomenndlem  46451  ovn0  46487  hsphoidmvle2  46506  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  hspdifhsp  46537  hoidifhspdmvle  46541  hspmbllem1  46547  hspmbllem2  46548  hspmbl  46550  volico2  46562  ovolval4lem2  46571  ovolval5lem1  46573  afvnfundmuv  47054  ndfatafv2  47126  prproropf1olem4  47380  suppmptcfin  48104  linc1  48154  ifnmfalse  48855