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

Theorem iffalse 4437
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 df-if 4429 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
2 dedlemb 1042 . . 3 𝜑 → (𝑥𝐵 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
32abbi2dv 2930 . 2 𝜑𝐵 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
41, 3eqtr4id 2855 1 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844   = wceq 1538  wcel 2112  {cab 2779  ifcif 4428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-if 4429
This theorem is referenced by:  iffalsei  4438  iffalsed  4439  ifnefalse  4440  ifsb  4441  ifbi  4449  ifeq1da  4458  ifeq12da  4460  ifclda  4462  ifeqda  4463  elimif  4464  ifbothda  4465  ifid  4467  ifnot  4478  ifan  4479  ifor  4480  2if2  4481  ifcomnan  4482  elimhyp  4491  elimhyp2v  4492  elimhyp3v  4493  elimhyp4v  4494  elimdhyp  4496  keephyp2v  4498  keephyp3v  4499  dfopif  4763  opprc  4791  somin1  5964  elimdelov  7233  ovif12  7236  oevn0  8127  pw2f1olem  8608  unxpdomlem2  8711  unxpdomlem3  8712  infsupprpr  8956  oi0  8980  wemaplem2  8999  ixpiunwdom  9042  cantnfp1lem3  9131  cantnflem1  9140  dfac12lem2  9559  fin23lem14  9748  axcc2lem  9851  ttukeylem5  9928  uzin  12270  xrmax1  12560  xrmax2  12561  xrmin1  12562  xrmin2  12563  max1ALT  12571  ifle  12582  xmulneg1  12654  modifeq2int  13300  seqf1olem1  13409  seqf1olem2  13410  bcval3  13666  swrdccat  14092  pfxccat3a  14095  swrdccat3b  14097  repswswrd  14141  cshword  14148  ccatco  14192  sumrblem  15063  fsumcvg  15064  summolem2a  15067  sumss  15076  fsumcvg2  15079  sumsplit  15118  prodeq2ii  15262  prodrblem  15278  fprodcvg  15279  prodmolem2a  15283  zprod  15286  prodss  15296  ruclem2  15580  ruclem3  15581  flodddiv4  15757  sadadd2lem2  15792  sadcp1  15797  sadcaddlem  15799  gcdn0val  15840  dfgcd2  15887  lcmn0val  15932  lcmfn0val  15960  pcgcd  16207  pcmptcl  16220  pcmpt  16221  pcmpt2  16222  pcprod  16224  fldivp1  16226  prmreclem2  16246  prmreclem4  16248  vdwlem6  16315  prmop1  16367  fvprmselelfz  16373  fvprmselgcd1  16374  ressval2  16548  xpsaddlem  16841  xpsvsca  16845  mreexexd  16914  setcepi  17343  pmtrmvd  18579  fincygsubgodd  19230  obselocv  20420  mvrf1  20666  mplcoe3  20709  mplmon2  20735  psrbagsn  20737  evlslem1  20757  mhpvarcl  20801  dmatmul  21105  1mavmul  21156  mulmarep1gsum2  21182  1marepvmarrepid  21183  mdetdiag  21207  mdetrsca2  21212  mdetrlin2  21215  mdetunilem5  21224  mdetunilem7  21226  mdetunilem8  21227  mdetunilem9  21228  mndifsplit  21244  maducoeval2  21248  madugsum  21251  madurid  21252  smadiadetglem2  21280  1elcpmat  21323  decpmatid  21378  ptpjpre1  22179  ptbasfi  22189  isfcls  22617  ptcmplem2  22661  ptcmplem3  22662  dscmet  23182  dscopn  23183  icccmplem2  23431  cnmpopc  23536  iccpnfcnv  23552  xrhmeo  23554  pcoval2  23624  pcopt  23630  pcopt2  23631  pcoass  23632  pcorevlem  23634  i1f1lem  24296  itg1addlem2  24304  itg1addlem3  24305  i1fres  24312  itg1climres  24321  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  itg2const2  24348  itg2seq  24349  itg2uba  24350  itg2splitlem  24355  itg2split  24356  itg2monolem1  24357  itg2gt0  24367  itg2cnlem1  24368  itg2cnlem2  24369  iblss  24411  iblss2  24412  itgle  24416  itgss  24418  ibladdlem  24426  itgaddlem1  24429  iblabslem  24434  iblabs  24435  iblabsr  24436  iblmulc2  24437  bddmulibl  24445  bddiblnc  24448  ditgneg  24463  elply2  24796  coeeq2  24842  dgrle  24843  coe1termlem  24858  logcnlem3  25238  igamgam  25637  isppw  25702  isnsqf  25723  mule1  25736  sqff1o  25770  chtublem  25798  dchrelbasd  25826  bposlem1  25871  bposlem3  25873  bposlem5  25875  bposlem6  25876  lgsneg  25908  lgsdilem  25911  lgsdir2  25917  lgsdir  25919  lgsdi  25921  lgsne0  25922  gausslemma2dlem1a  25952  2lgslem1c  25980  2lgs  25994  dchrvmasum2if  26084  ostth2lem4  26223  axlowdimlem15  26753  elimifd  30313  elim2if  30314  ifeq3da  30316  imadifxp  30367  pmtridf1o  30789  resvval2  30956  xrge0iifcnv  31284  indval2  31381  ddeval0  31602  eulerpartlemb  31734  plymulx0  31925  signsw0glem  31931  signswmnd  31935  dfrdg2  33148  dfrdg3  33149  noprefixmo  33310  nosupno  33311  nosupdm  33312  nosupbday  33313  nosupfv  33314  nosupres  33315  nosupbnd1lem1  33316  unisnif  33494  dfrdg4  33520  bj-xpima1sn  34387  finxpreclem2  34802  finxpreclem5  34807  matunitlindflem1  35046  poimirlem15  35065  poimirlem23  35073  mbfposadd  35097  itg2addnclem  35101  itg2addnclem3  35103  itg2gt0cn  35105  ibladdnclem  35106  itgaddnclem1  35108  iblabsnclem  35113  iblabsnc  35114  iblmulc2nc  35115  ftc1anclem5  35127  ftc1anclem7  35129  ftc1anclem8  35130  ftc1anc  35131  areacirclem5  35142  areacirc  35143  heiborlem4  35245  ac6s6  35603  riotaclbgBAD  36243  cdleme27a  37656  cdleme31sn2  37678  dihvalc  38522  mapdhval2  39015  hdmap1val2  39089  metakunt6  39346  metakunt7  39347  metakunt8  39348  metakunt11  39351  metakunt12  39352  metakunt22  39362  fsuppind  39443  dffltz  39602  pw2f1ocnv  39965  aomclem5  39989  arearect  40152  areaquad  40153  upbdrech2  41927  lptioo2  42260  lptioo1  42261  limsupmnfuzlem  42355  limsupre3uzlem  42364  limsup10exlem  42401  coskpi2  42495  cosknegpi  42498  icccncfext  42516  cncfiooicclem1  42522  cncfiooiccre  42524  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  itgioocnicc  42606  iblcncfioo  42607  volico  42612  sublevolico  42613  voliooico  42621  voliccico  42628  dirkerper  42725  dirkertrigeq  42730  dirkercncflem2  42733  fourierdlem10  42746  fourierdlem32  42768  fourierdlem33  42769  fourierdlem37  42773  fourierdlem62  42797  fourierdlem73  42808  fourierdlem74  42809  fourierdlem75  42810  fourierdlem79  42814  fourierdlem81  42816  fourierdlem82  42817  fourierdlem93  42828  fourierdlem97  42832  fourierdlem101  42836  fourierdlem103  42838  fourierdlem104  42839  sqwvfoura  42857  sqwvfourb  42858  fourierswlem  42859  fouriersw  42860  elaa2lem  42862  etransclem15  42878  etransclem19  42882  etransclem23  42886  etransclem24  42887  etransclem25  42888  ioorrnopnxrlem  42935  nnfoctbdjlem  43081  isomenndlem  43156  ovn0  43192  hsphoidmvle2  43211  hoidmv1lelem1  43217  hoidmv1lelem2  43218  hoidmv1le  43220  hoidmvlelem2  43222  hoidmvlelem3  43223  ovnhoilem1  43227  hspdifhsp  43242  hoidifhspdmvle  43246  hspmbllem1  43252  hspmbllem2  43253  hspmbl  43255  volico2  43267  ovolval4lem2  43276  ovolval5lem1  43278  afvnfundmuv  43682  ndfatafv2  43754  prproropf1olem4  44010  suppmptcfin  44768  linc1  44821  ifnmfalse  45276
  Copyright terms: Public domain W3C validator