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  4337  opprc  4362  somin1  5448  dfiota4  5796  elimdelov  6634  ovif12  6637  oevn0  7482  pw2f1olem  7949  unxpdomlem2  8050  unxpdomlem3  8051  oi0  8316  wemaplem2  8335  ixpiunwdom  8379  cantnfp1lem3  8460  cantnflem1  8469  dfac12lem2  8849  fin23lem14  9038  axcc2lem  9141  ttukeylem5  9218  uzin  11596  xrmax1  11880  xrmax2  11881  xrmin1  11882  xrmin2  11883  max1ALT  11891  ifle  11902  xmulneg1  11971  modifeq2int  12594  seqf1olem1  12702  seqf1olem2  12703  bcval3  12955  swrdccat  13344  swrdccat3a  13345  swrdccat3b  13347  repswswrd  13382  cshword  13388  ccatco  13432  sumrblem  14289  fsumcvg  14290  summolem2a  14293  sumss  14302  fsumcvg2  14305  sumsplit  14341  prodeq2ii  14482  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  prodss  14516  ruclem2  14800  ruclem3  14801  flodddiv4  14975  sadadd2lem2  15010  sadcp1  15015  sadcaddlem  15017  gcdn0val  15058  dfgcd2  15101  lcmn0val  15146  lcmfn0val  15174  pcgcd  15420  pcmptcl  15433  pcmpt  15434  pcmpt2  15435  pcprod  15437  fldivp1  15439  prmreclem2  15459  prmreclem4  15461  vdwlem6  15528  prmo1  15579  prmop1  15580  fvprmselelfz  15586  fvprmselgcd1  15587  ressval2  15756  xpsaddlem  16058  xpsvsca  16062  mreexexd  16131  setcepi  16561  pmtrmvd  17699  mvrf1  19246  mplcoe3  19287  mplmon2  19314  psrbagsn  19316  evlslem1  19336  obselocv  19891  dmatmul  20122  1mavmul  20173  mulmarep1gsum2  20199  1marepvmarrepid  20200  mdetdiag  20224  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  mndifsplit  20261  maducoeval2  20265  madugsum  20268  madurid  20269  smadiadetglem2  20297  1elcpmat  20339  decpmatid  20394  ptpjpre1  21184  ptbasfi  21194  isfcls  21623  ptcmplem2  21667  ptcmplem3  21668  dscmet  22187  dscopn  22188  icccmplem2  22434  cnmpt2pc  22535  iccpnfcnv  22551  xrhmeo  22553  pcoval2  22624  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  i1f1lem  23262  itg1addlem2  23270  itg1addlem3  23271  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  iblss  23377  iblss2  23378  itgle  23382  itgss  23384  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  bddmulibl  23411  ditgneg  23427  elply2  23756  coeeq2  23802  dgrle  23803  coe1termlem  23818  logcnlem3  24190  igamgam  24575  isppw  24640  isnsqf  24661  mule1  24674  sqff1o  24708  chtublem  24736  dchrelbasd  24764  bposlem1  24809  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgsneg  24846  lgsdilem  24849  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsne0  24860  gausslemma2dlem1a  24890  2lgslem1c  24918  2lgs  24932  dchrvmasum2if  24986  ostth2lem4  25125  axlowdimlem15  25636  elimifd  28746  elim2if  28747  imadifxp  28796  resvval2  29160  xrge0iifcnv  29307  indval2  29404  ddeval0  29625  eulerpartlemb  29757  plymulx0  29950  signsw0glem  29956  signswmnd  29960  dfrdg2  30945  dfrdg3  30946  unisnif  31202  dfrdg4  31228  bj-xpima1sn  32136  finxpreclem2  32403  finxpreclem5  32408  matunitlindflem1  32575  poimirlem15  32594  poimirlem23  32602  mbfposadd  32627  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  bddiblnc  32650  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem5  32674  areacirc  32675  heiborlem4  32783  ac6s6  33150  riotaclbgBAD  33258  cdleme27a  34673  cdleme31sn2  34695  dihvalc  35540  mapdhval2  36033  hdmap1val2  36108  pw2f1ocnv  36622  aomclem5  36646  arearect  36820  areaquad  36821  upbdrech2  38463  lptioo2  38698  lptioo1  38699  coskpi2  38749  cosknegpi  38752  icccncfext  38773  cncfiooicclem1  38779  cncfiooiccre  38781  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  itgioocnicc  38869  iblcncfioo  38870  volico  38876  sublevolico  38877  voliooico  38885  voliccico  38892  dirkerper  38989  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem10  39010  fourierdlem32  39032  fourierdlem33  39033  fourierdlem37  39037  fourierdlem62  39061  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem15  39142  etransclem19  39146  etransclem23  39150  etransclem24  39151  etransclem25  39152  ioorrnopnxrlem  39202  nnfoctbdjlem  39348  isomenndlem  39420  ovn0  39456  hsphoidmvle2  39475  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  hspdifhsp  39506  hoidifhspdmvle  39510  hspmbllem1  39516  hspmbllem2  39517  hspmbl  39519  volico2  39531  ovolval4lem2  39540  ovolval5lem1  39542  afvnfundmuv  39868  pfxccat3a  40292  cshword2  40300  suppmptcfin  41954  linc1  42008  ifnmfalse  42303
  Copyright terms: Public domain W3C validator