MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iffalse Structured version   Visualization version   GIF version

Theorem iffalse 4128
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.
StepHypRef Expression
1 dedlemb 1015 . . 3 𝜑 → (𝑥𝐵 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
21abbi2dv 2771 . 2 𝜑𝐵 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
3 df-if 4120 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
42, 3syl6reqr 2704 1 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1523  wcel 2030  {cab 2637  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  iffalsei  4129  iffalsed  4130  ifnefalse  4131  ifsb  4132  ifbi  4140  ifeq1da  4149  ifeq12da  4151  ifclda  4153  ifeqda  4154  elimif  4155  ifbothda  4156  ifid  4158  ifnot  4166  ifan  4167  ifor  4168  2if2  4169  ifcomnan  4170  elimhyp  4179  elimhyp2v  4180  elimhyp3v  4181  elimhyp4v  4182  elimdhyp  4184  keephyp2v  4186  keephyp3v  4187  dfopif  4430  opprc  4456  somin1  5564  dfiota4OLD  5918  elimdelov  6778  ovif12  6781  oevn0  7640  pw2f1olem  8105  unxpdomlem2  8206  unxpdomlem3  8207  oi0  8474  wemaplem2  8493  ixpiunwdom  8537  cantnfp1lem3  8615  cantnflem1  8624  dfac12lem2  9004  fin23lem14  9193  axcc2lem  9296  ttukeylem5  9373  uzin  11758  xrmax1  12044  xrmax2  12045  xrmin1  12046  xrmin2  12047  max1ALT  12055  ifle  12066  xmulneg1  12137  modifeq2int  12772  seqf1olem1  12880  seqf1olem2  12881  bcval3  13133  swrdccat  13539  swrdccat3a  13540  swrdccat3b  13542  repswswrd  13577  cshword  13583  ccatco  13627  sumrblem  14486  fsumcvg  14487  summolem2a  14490  sumss  14499  fsumcvg2  14502  sumsplit  14543  prodeq2ii  14687  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  zprod  14711  prodss  14721  ruclem2  15005  ruclem3  15006  flodddiv4  15184  sadadd2lem2  15219  sadcp1  15224  sadcaddlem  15226  gcdn0val  15267  dfgcd2  15310  lcmn0val  15355  lcmfn0val  15383  pcgcd  15629  pcmptcl  15642  pcmpt  15643  pcmpt2  15644  pcprod  15646  fldivp1  15648  prmreclem2  15668  prmreclem4  15670  vdwlem6  15737  prmo1  15788  prmop1  15789  fvprmselelfz  15795  fvprmselgcd1  15796  ressval2  15976  xpsaddlem  16282  xpsvsca  16286  mreexexd  16355  setcepi  16785  pmtrmvd  17922  mvrf1  19473  mplcoe3  19514  mplmon2  19541  psrbagsn  19543  evlslem1  19563  obselocv  20120  dmatmul  20351  1mavmul  20402  mulmarep1gsum2  20428  1marepvmarrepid  20429  mdetdiag  20453  mdetrsca2  20458  mdetrlin2  20461  mdetunilem5  20470  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  mndifsplit  20490  maducoeval2  20494  madugsum  20497  madurid  20498  smadiadetglem2  20526  1elcpmat  20568  decpmatid  20623  ptpjpre1  21422  ptbasfi  21432  isfcls  21860  ptcmplem2  21904  ptcmplem3  21905  dscmet  22424  dscopn  22425  icccmplem2  22673  cnmpt2pc  22774  iccpnfcnv  22790  xrhmeo  22792  pcoval2  22862  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  i1f1lem  23501  itg1addlem2  23509  itg1addlem3  23510  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  iblss  23616  iblss2  23617  itgle  23621  itgss  23623  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  bddmulibl  23650  ditgneg  23666  elply2  23997  coeeq2  24043  dgrle  24044  coe1termlem  24059  logcnlem3  24435  igamgam  24820  isppw  24885  isnsqf  24906  mule1  24919  sqff1o  24953  chtublem  24981  dchrelbasd  25009  bposlem1  25054  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgsneg  25091  lgsdilem  25094  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsne0  25105  gausslemma2dlem1a  25135  2lgslem1c  25163  2lgs  25177  dchrvmasum2if  25231  ostth2lem4  25370  axlowdimlem15  25881  elimifd  29488  elim2if  29489  ifeq3da  29491  imadifxp  29540  resvval2  29957  pmtridf1o  29984  xrge0iifcnv  30107  indval2  30204  ddeval0  30426  eulerpartlemb  30558  plymulx0  30752  signsw0glem  30758  signswmnd  30762  dfrdg2  31825  dfrdg3  31826  noprefixmo  31973  nosupno  31974  nosupdm  31975  nosupbday  31976  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  unisnif  32157  dfrdg4  32183  bj-xpima1sn  33068  finxpreclem2  33357  finxpreclem5  33362  matunitlindflem1  33535  poimirlem15  33554  poimirlem23  33562  mbfposadd  33587  itg2addnclem  33591  itg2addnclem3  33593  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  bddiblnc  33610  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem5  33634  areacirc  33635  heiborlem4  33743  ac6s6  34110  riotaclbgBAD  34558  cdleme27a  35972  cdleme31sn2  35994  dihvalc  36839  mapdhval2  37332  hdmap1val2  37407  pw2f1ocnv  37921  aomclem5  37945  arearect  38118  areaquad  38119  upbdrech2  39836  lptioo2  40181  lptioo1  40182  limsupmnfuzlem  40276  limsupre3uzlem  40285  limsup10exlem  40322  coskpi2  40395  cosknegpi  40398  icccncfext  40418  cncfiooicclem1  40424  cncfiooiccre  40426  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  itgioocnicc  40511  iblcncfioo  40512  volico  40518  sublevolico  40519  voliooico  40527  voliccico  40534  dirkerper  40631  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem10  40652  fourierdlem32  40674  fourierdlem33  40675  fourierdlem37  40679  fourierdlem62  40703  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem93  40734  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem15  40784  etransclem19  40788  etransclem23  40792  etransclem24  40793  etransclem25  40794  ioorrnopnxrlem  40844  nnfoctbdjlem  40990  isomenndlem  41065  ovn0  41101  hsphoidmvle2  41120  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  hspdifhsp  41151  hoidifhspdmvle  41155  hspmbllem1  41161  hspmbllem2  41162  hspmbl  41164  volico2  41176  ovolval4lem2  41185  ovolval5lem1  41187  afvnfundmuv  41540  pfxccat3a  41754  cshword2  41762  suppmptcfin  42485  linc1  42539  ifnmfalse  42832
  Copyright terms: Public domain W3C validator