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

Theorem iftrue 4125
Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
iftrue (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrue
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dedlem0a 1012 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2771 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4121 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2704 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  iftruei  4126  iftrued  4127  ifsb  4132  ifbi  4140  ifeq2da  4150  ifeq12da  4151  ifclda  4153  ifeqda  4154  elimif  4155  ifbothda  4156  ifid  4158  ifeqor  4165  ifnot  4166  ifan  4167  ifor  4168  2if2  4169  dedth  4172  elimhyp  4179  elimhyp2v  4180  elimhyp3v  4181  elimhyp4v  4182  elimdhyp  4184  keephyp2v  4186  keephyp3v  4187  dfopif  4430  dfopg  4431  somin1  5564  somincom  5565  xpima1  5612  dfiota4OLD  5918  elimdelov  6778  ovif12  6781  tz7.44-1  7547  resixpfo  7988  boxriin  7992  boxcutc  7993  pw2f1olem  8105  unxpdomlem2  8206  unxpdomlem3  8207  ordtypelem1  8464  wemaplem2  8493  unwdomg  8530  ixpiunwdom  8537  cantnfp1lem2  8614  cantnfp1lem3  8615  acndom  8912  dfac12lem2  9004  fin23lem14  9193  axcc2lem  9296  pwfseqlem2  9519  uzin  11758  xrmax1  12044  xrmax2  12045  xrmin1  12046  xrmin2  12047  max1ALT  12055  max0sub  12065  ifle  12066  xmulneg1  12137  fzprval  12439  fztpval  12440  modifeq2int  12772  seqf1olem1  12880  seqf1olem2  12881  bcval2  13132  ccatval1  13395  ccatalpha  13411  swrdccat  13539  swrdccat3a  13540  swrdccat3b  13542  repswswrd  13577  cshword  13583  0csh0  13585  ccatco  13627  sgnn  13878  max0add  14094  absmax  14113  sumrblem  14486  fsumcvg  14487  summolem2a  14490  isum  14494  sumss  14499  sumss2  14501  fsumcvg2  14502  fsumser  14505  fsumsplit  14515  sumsplit  14543  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  zprod  14711  iprod  14712  iprodn0  14714  prodss  14721  fprodsplit  14740  ruclem2  15005  ruclem3  15006  flodddiv4  15184  sadadd2lem2  15219  sadcf  15222  sadc0  15223  sadcp1  15224  sadcaddlem  15226  smupf  15247  smup0  15248  gcd0val  15266  dfgcd2  15310  eucalgf  15343  eucalginv  15344  eucalglt  15345  lcmf0val  15382  phisum  15542  pc0  15606  pcgcd  15629  pcmptcl  15642  pcmpt  15643  pcmpt2  15644  pcprod  15646  fldivp1  15648  prmreclem2  15668  prmreclem4  15670  1arithlem4  15677  vdwlem6  15737  ramtcl2  15762  ramcl2  15767  ramub1lem1  15777  prmop1  15789  fvprmselelfz  15795  fvprmselgcd1  15796  ressid2  15975  xpscfv  16269  xpsfrnel  16270  xpsaddlem  16282  xpsvsca  16286  mreexexd  16355  gsumval1  17324  mgm2nsgrplem2  17453  sgrp2nmndlem2  17458  symgextfve  17885  symgfixfolem1  17904  pmtrmvd  17922  pmtrfinv  17927  pmtrprfval  17953  pmtrprfvalrn  17954  frgpuptinv  18230  frgpup2  18235  frgpup3lem  18236  cyggex  18345  gsumzsplit  18373  gsummpt1n0  18410  dprdfid  18462  dmdprdsplitlem  18482  abvtrivd  18888  psrlidm  19451  psrridm  19452  mvrf1  19473  mplmonmul  19512  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  mplmon2  19541  subrgasclcl  19547  evlslem3  19562  evlslem1  19563  coe1tmfv1  19692  ply1sclid  19706  znf1o  19948  uvcvv1  20176  dmatmul  20351  scmatscmiddistr  20362  1mavmul  20402  mulmarep1gsum2  20428  1marepvmarrepid  20429  mdetdiag  20453  mdetralt2  20463  mdetunilem2  20467  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  mndifsplit  20490  maducoeval2  20494  madugsum  20497  madurid  20498  gsummatr01lem3  20511  gsummatr01  20513  smadiadetglem2  20526  1elcpmat  20568  decpmatid  20623  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  ptpjpre1  21422  ptbasfi  21432  ptpjopn  21463  isfcls  21860  ptcmplem2  21904  ptcmplem3  21905  tsmssplit  22002  dscmet  22424  dscopn  22425  icccmplem2  22673  iccpnfcnv  22790  xrhmeo  22792  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  cmetcaulem  23132  ovolicc1  23330  ioorcl  23391  i1f1lem  23501  itg11  23503  itg1addlem2  23509  itg1addlem4  23511  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1flim  23535  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2cnlem1  23573  itg2cnlem2  23574  iblcnlem  23600  iblss  23616  iblss2  23617  itgitg2  23618  itgle  23621  itgss  23623  itgss2  23624  itgss3  23626  itgless  23628  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  bddmulibl  23650  itggt0  23653  itgcn  23654  limcvallem  23680  ellimc2  23686  limccnp  23700  limccnp2  23701  limcco  23702  dvcobr  23754  dvexp2  23762  elply2  23997  elplyd  24003  ply1termlem  24004  coe1termlem  24059  abelthlem9  24239  logtayl  24451  leibpilem2  24713  leibpi  24714  rlimcnp2  24738  efrlim  24741  igamz  24819  isnsqf  24906  mule1  24919  sqff1o  24953  muinv  24964  chtublem  24981  dchrelbasd  25009  bposlem1  25054  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgsval2lem  25077  lgsneg  25091  lgsdilem  25094  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsne0  25105  gausslemma2dlem1a  25135  2lgslem1c  25163  2lgslem3  25174  2lgs  25177  dchrvmasum2if  25231  dchrvmasumiflem1  25235  rpvmasum2  25246  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  padicabv  25364  ostth2lem4  25370  axlowdimlem15  25881  opvtxval  25928  opiedgval  25931  elimifd  29488  elim2if  29489  ifeq3da  29491  resvid2  29956  fzto1stfv1  29979  pmtridf1o  29984  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  indval2  30204  ind1  30207  sigaclfu2  30312  ddeval1  30425  eulerpartlemb  30558  ballotlemsima  30705  ballotlemrv1  30710  signsw0glem  30758  signswmnd  30762  signswrid  30763  indispconn  31342  mrsubvr  31534  dfrdg2  31825  dfrdg3  31826  noprefixmo  31973  nosupno  31974  nosupbday  31976  nosupbnd1  31985  nosupbnd2  31987  unisnif  32157  dfrdg4  32183  fnejoin2  32489  unbdqndv2lem2  32626  bj-xpima2sn  33070  finxpreclem1  33356  finxpreclem3  33360  matunitlindflem1  33535  poimirlem2  33541  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  mblfinlem2  33577  mbfposadd  33587  itg2addnclem  33591  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  bddiblnc  33610  itggt0cn  33612  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem5  33634  areacirc  33635  fdc  33671  heiborlem4  33743  ac6s6  34110  cdleme27a  35972  cdleme31sn1  35986  cdleme31fv1  35996  cdlemk40t  36523  dihvalb  36843  pw2f1ocnv  37921  aomclem5  37945  kelac1  37950  sdrgacs  38088  mon1pid  38100  arearect  38118  areaquad  38119  clsk1indlem1  38660  refsum2cnlem1  39510  upbdrech2  39836  lptioo2  40181  lptioo1  40182  limsupmnfuzlem  40276  limsupre3uzlem  40285  limsup10exlem  40322  coskpi2  40395  cosknegpi  40398  cncfiooicclem1  40424  cncfiooiccre  40426  dvnxpaek  40475  dvnprodlem1  40479  dvnprodlem3  40481  itgioocnicc  40511  iblcncfioo  40512  volico  40518  sublevolico  40519  volioore  40525  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  etransclem4  40773  etransclem15  40784  etransclem19  40788  etransclem20  40789  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem27  40796  etransclem31  40800  etransclem32  40801  ioorrnopnxrlem  40844  nnfoctbdjlem  40990  isomenndlem  41065  ovn0val  41085  hoidmv0val  41118  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  ovnsubadd2lem  41180  ovolval4lem2  41185  ovolval5lem1  41187  afvfundmfveq  41539  pfxccat3a  41754  cshword2  41762  linc1  42539  lincext3  42570  lindslinindsimp1  42571  el0ldep  42580  islindeps2  42597
  Copyright terms: Public domain W3C validator