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

Theorem iffalse 4045
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 994 . . 3 𝜑 → (𝑥𝐵 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
21abbi2dv 2729 . 2 𝜑𝐵 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
3 df-if 4037 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
42, 3syl6reqr 2663 1 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1475  wcel 1977  {cab 2596  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037
This theorem is referenced by:  iffalsei  4046  iffalsed  4047  ifnefalse  4048  ifsb  4049  ifbi  4057  ifeq1da  4066  ifeq12da  4068  ifclda  4070  ifeqda  4071  elimif  4072  ifbothda  4073  ifid  4075  ifnot  4083  ifan  4084  ifor  4085  2if2  4086  ifcomnan  4087  elimhyp  4096  elimhyp2v  4097  elimhyp3v  4098  elimhyp4v  4099  elimdhyp  4101  keephyp2v  4103  keephyp3v  4104  dfopif  4332  opprc  4357  somin1  5435  dfiota4  5782  elimdelov  6612  ovif12  6615  oevn0  7460  pw2f1olem  7927  unxpdomlem2  8028  unxpdomlem3  8029  oi0  8294  wemaplem2  8313  ixpiunwdom  8357  cantnfp1lem3  8438  cantnflem1  8447  dfac12lem2  8827  fin23lem14  9016  axcc2lem  9119  ttukeylem5  9196  uzin  11555  xrmax1  11842  xrmax2  11843  xrmin1  11844  xrmin2  11845  max1ALT  11853  ifle  11864  xmulneg1  11931  modifeq2int  12552  seqf1olem1  12660  seqf1olem2  12661  bcval3  12913  swrdccat  13293  swrdccat3a  13294  swrdccat3b  13296  repswswrd  13331  cshword  13337  ccatco  13381  sumrblem  14238  fsumcvg  14239  summolem2a  14242  sumss  14251  fsumcvg2  14254  sumsplit  14290  prodeq2ii  14431  prodrblem  14447  fprodcvg  14448  prodmolem2a  14452  zprod  14455  prodss  14465  ruclem2  14749  ruclem3  14750  flodddiv4  14924  sadadd2lem2  14959  sadcp1  14964  sadcaddlem  14966  gcdn0val  15007  dfgcd2  15050  lcmn0val  15095  lcmfn0val  15123  pcgcd  15369  pcmptcl  15382  pcmpt  15383  pcmpt2  15384  pcprod  15386  fldivp1  15388  prmreclem2  15408  prmreclem4  15410  vdwlem6  15477  prmo1  15528  prmop1  15529  fvprmselelfz  15535  fvprmselgcd1  15536  ressval2  15705  xpsaddlem  16007  xpsvsca  16011  mreexexd  16080  setcepi  16510  pmtrmvd  17648  mvrf1  19195  mplcoe3  19236  mplmon2  19263  psrbagsn  19265  evlslem1  19285  obselocv  19839  dmatmul  20070  1mavmul  20121  mulmarep1gsum2  20147  1marepvmarrepid  20148  mdetdiag  20172  mdetrsca2  20177  mdetrlin2  20180  mdetunilem5  20189  mdetunilem7  20191  mdetunilem8  20192  mdetunilem9  20193  mndifsplit  20209  maducoeval2  20213  madugsum  20216  madurid  20217  smadiadetglem2  20245  1elcpmat  20287  decpmatid  20342  ptpjpre1  21132  ptbasfi  21142  isfcls  21571  ptcmplem2  21615  ptcmplem3  21616  dscmet  22135  dscopn  22136  icccmplem2  22382  cnmpt2pc  22483  iccpnfcnv  22499  xrhmeo  22501  pcoval2  22572  pcohtpylem  22575  pcopt  22578  pcopt2  22579  pcoass  22580  pcorevlem  22582  i1f1lem  23207  itg1addlem2  23215  itg1addlem3  23216  i1fres  23223  itg1climres  23232  mbfi1fseqlem4  23236  mbfi1fseqlem5  23237  itg2const2  23259  itg2seq  23260  itg2uba  23261  itg2splitlem  23266  itg2split  23267  itg2monolem1  23268  itg2gt0  23278  itg2cnlem1  23279  itg2cnlem2  23280  iblss  23322  iblss2  23323  itgle  23327  itgss  23329  ibladdlem  23337  itgaddlem1  23340  iblabslem  23345  iblabs  23346  iblabsr  23347  iblmulc2  23348  bddmulibl  23356  ditgneg  23372  elply2  23701  coeeq2  23747  dgrle  23748  coe1termlem  23763  logcnlem3  24135  igamgam  24520  isppw  24585  isnsqf  24606  mule1  24619  sqff1o  24653  chtublem  24681  dchrelbasd  24709  bposlem1  24754  bposlem3  24756  bposlem5  24758  bposlem6  24759  lgsneg  24791  lgsdilem  24794  lgsdir2  24800  lgsdir  24802  lgsdi  24804  lgsne0  24805  gausslemma2dlem1a  24835  2lgslem1c  24863  2lgs  24877  dchrvmasum2if  24931  ostth2lem4  25070  axlowdimlem15  25582  elimifd  28540  elim2if  28541  imadifxp  28590  resvval2  28954  xrge0iifcnv  29101  indval2  29198  ddeval0  29419  eulerpartlemb  29551  plymulx0  29744  signsw0glem  29750  signswmnd  29754  dfrdg2  30739  dfrdg3  30740  unisnif  30996  dfrdg4  31022  bj-xpima1sn  31930  finxpreclem2  32197  finxpreclem5  32202  matunitlindflem1  32369  poimirlem15  32388  poimirlem23  32396  mbfposadd  32421  itg2addnclem  32425  itg2addnclem3  32427  itg2gt0cn  32429  ibladdnclem  32430  itgaddnclem1  32432  iblabsnclem  32437  iblabsnc  32438  iblmulc2nc  32439  bddiblnc  32444  ftc1anclem5  32453  ftc1anclem7  32455  ftc1anclem8  32456  ftc1anc  32457  areacirclem5  32468  areacirc  32469  heiborlem4  32577  ac6s6  32944  riotaclbgBAD  33052  cdleme27a  34467  cdleme31sn2  34489  dihvalc  35334  mapdhval2  35827  hdmap1val2  35902  pw2f1ocnv  36416  aomclem5  36440  arearect  36614  areaquad  36615  upbdrech2  38257  lptioo2  38492  lptioo1  38493  coskpi2  38543  cosknegpi  38546  icccncfext  38567  cncfiooicclem1  38573  cncfiooiccre  38575  ioodvbdlimc1lem2  38616  ioodvbdlimc2lem  38618  itgioocnicc  38663  iblcncfioo  38664  volico  38670  sublevolico  38671  voliooico  38679  voliccico  38686  dirkerper  38783  dirkertrigeq  38788  dirkercncflem2  38791  fourierdlem10  38804  fourierdlem32  38826  fourierdlem33  38827  fourierdlem37  38831  fourierdlem62  38855  fourierdlem73  38866  fourierdlem74  38867  fourierdlem75  38868  fourierdlem79  38872  fourierdlem81  38874  fourierdlem82  38875  fourierdlem93  38886  fourierdlem97  38890  fourierdlem101  38894  fourierdlem103  38896  fourierdlem104  38897  sqwvfoura  38915  sqwvfourb  38916  fourierswlem  38917  fouriersw  38918  elaa2lem  38920  etransclem15  38936  etransclem19  38940  etransclem23  38944  etransclem24  38945  etransclem25  38946  ioorrnopnxrlem  38996  nnfoctbdjlem  39142  isomenndlem  39214  ovn0  39250  hsphoidmvle2  39269  hoidmv1lelem1  39275  hoidmv1lelem2  39276  hoidmv1le  39278  hoidmvlelem2  39280  hoidmvlelem3  39281  ovnhoilem1  39285  hspdifhsp  39300  hoidifhspdmvle  39304  hspmbllem1  39310  hspmbllem2  39311  hspmbl  39313  volico2  39325  ovolval4lem2  39334  ovolval5lem1  39336  afvnfundmuv  39663  pfxccat3a  40087  cshword2  40095  suppmptcfin  41946  linc1  42000  ifnmfalse  42256
  Copyright terms: Public domain W3C validator