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

Theorem iftrue 4064
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 999 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2739 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4060 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2674 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  {cab 2607  ifcif 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4059
This theorem is referenced by:  iftruei  4065  iftrued  4066  ifsb  4071  ifbi  4079  ifeq2da  4089  ifeq12da  4090  ifclda  4092  ifeqda  4093  elimif  4094  ifbothda  4095  ifid  4097  ifeqor  4104  ifnot  4105  ifan  4106  ifor  4107  2if2  4108  dedth  4111  elimhyp  4118  elimhyp2v  4119  elimhyp3v  4120  elimhyp4v  4121  elimdhyp  4123  keephyp2v  4125  keephyp3v  4126  dfopif  4367  dfopg  4368  somin1  5488  somincom  5489  xpima1  5536  dfiota4OLD  5839  elimdelov  6689  ovif12  6692  tz7.44-1  7447  resixpfo  7890  boxriin  7894  boxcutc  7895  pw2f1olem  8008  unxpdomlem2  8109  unxpdomlem3  8110  ordtypelem1  8367  wemaplem2  8396  unwdomg  8433  ixpiunwdom  8440  cantnfp1lem2  8520  cantnfp1lem3  8521  acndom  8818  dfac12lem2  8910  fin23lem14  9099  axcc2lem  9202  pwfseqlem2  9425  uzin  11664  xrmax1  11949  xrmax2  11950  xrmin1  11951  xrmin2  11952  max1ALT  11960  max0sub  11970  ifle  11971  xmulneg1  12042  fzprval  12343  fztpval  12344  modifeq2int  12672  seqf1olem1  12780  seqf1olem2  12781  bcval2  13032  ccatval1  13300  ccatalpha  13314  swrdccat  13430  swrdccat3a  13431  swrdccat3b  13433  repswswrd  13468  cshword  13474  0csh0  13476  ccatco  13518  sgnn  13768  max0add  13984  absmax  14003  sumrblem  14375  fsumcvg  14376  summolem2a  14379  isum  14383  sumss  14388  sumss2  14390  fsumcvg2  14391  fsumser  14394  fsumsplit  14404  sumsplit  14427  prodrblem  14584  fprodcvg  14585  prodmolem2a  14589  zprod  14592  iprod  14593  iprodn0  14595  prodss  14602  fprodsplit  14621  ruclem2  14886  ruclem3  14887  flodddiv4  15061  sadadd2lem2  15096  sadcf  15099  sadc0  15100  sadcp1  15101  sadcaddlem  15103  smupf  15124  smup0  15125  gcd0val  15143  dfgcd2  15187  eucalgf  15220  eucalginv  15221  eucalglt  15222  lcmf0val  15259  phisum  15419  pc0  15483  pcgcd  15506  pcmptcl  15519  pcmpt  15520  pcmpt2  15521  pcprod  15523  fldivp1  15525  prmreclem2  15545  prmreclem4  15547  1arithlem4  15554  vdwlem6  15614  ramtcl2  15639  ramcl2  15644  ramub1lem1  15654  prmop1  15666  fvprmselelfz  15672  fvprmselgcd1  15673  ressid2  15849  xpscfv  16143  xpsfrnel  16144  xpsaddlem  16156  xpsvsca  16160  mreexexd  16229  gsumval1  17198  mgm2nsgrplem2  17327  sgrp2nmndlem2  17332  symgextfve  17760  symgfixfolem1  17779  pmtrmvd  17797  pmtrfinv  17802  pmtrprfval  17828  pmtrprfvalrn  17829  frgpuptinv  18105  frgpup2  18110  frgpup3lem  18111  cyggex  18220  gsumzsplit  18248  gsummpt1n0  18285  dprdfid  18337  dmdprdsplitlem  18357  abvtrivd  18761  psrlidm  19322  psrridm  19323  mvrf1  19344  mplmonmul  19383  mplcoe1  19384  mplcoe3  19385  mplcoe5  19387  mplmon2  19412  subrgasclcl  19418  evlslem3  19433  evlslem1  19434  coe1tmfv1  19563  ply1sclid  19577  znf1o  19819  uvcvv1  20047  dmatmul  20222  scmatscmiddistr  20233  1mavmul  20273  mulmarep1gsum2  20299  1marepvmarrepid  20300  mdetdiag  20324  mdetralt2  20334  mdetunilem2  20338  mdetunilem7  20343  mdetunilem8  20344  mdetunilem9  20345  mndifsplit  20361  maducoeval2  20365  madugsum  20368  madurid  20369  gsummatr01lem3  20382  gsummatr01  20384  smadiadetglem2  20397  1elcpmat  20439  decpmatid  20494  chfacfscmulgsum  20584  chfacfpmmulgsum  20588  ptpjpre1  21284  ptbasfi  21294  ptpjopn  21325  isfcls  21723  ptcmplem2  21767  ptcmplem3  21768  tsmssplit  21865  dscmet  22287  dscopn  22288  icccmplem2  22534  iccpnfcnv  22651  xrhmeo  22653  pcohtpylem  22727  pcopt  22730  pcopt2  22731  pcoass  22732  pcorevlem  22734  cmetcaulem  22994  ovolicc1  23191  ioorcl  23251  i1f1lem  23362  itg11  23364  itg1addlem2  23370  itg1addlem4  23372  i1fres  23378  itg1climres  23387  mbfi1fseqlem4  23391  mbfi1fseqlem5  23392  mbfi1flim  23396  itg2const2  23414  itg2seq  23415  itg2uba  23416  itg2splitlem  23421  itg2split  23422  itg2monolem1  23423  itg2cnlem1  23434  itg2cnlem2  23435  iblcnlem  23461  iblss  23477  iblss2  23478  itgitg2  23479  itgle  23482  itgss  23484  itgss2  23485  itgss3  23487  itgless  23489  ibladdlem  23492  itgaddlem1  23495  iblabslem  23500  iblabs  23501  iblabsr  23502  iblmulc2  23503  bddmulibl  23511  itggt0  23514  itgcn  23515  limcvallem  23541  ellimc2  23547  limccnp  23561  limccnp2  23562  limcco  23563  dvcobr  23615  dvexp2  23623  elply2  23856  elplyd  23862  ply1termlem  23863  coe1termlem  23918  abelthlem9  24098  logtayl  24306  leibpilem2  24568  leibpi  24569  rlimcnp2  24593  efrlim  24596  igamz  24674  isnsqf  24761  mule1  24774  sqff1o  24808  muinv  24819  chtublem  24836  dchrelbasd  24864  bposlem1  24909  bposlem3  24911  bposlem5  24913  bposlem6  24914  lgsval2lem  24932  lgsneg  24946  lgsdilem  24949  lgsdir2  24955  lgsdir  24957  lgsdi  24959  lgsne0  24960  gausslemma2dlem1a  24990  2lgslem1c  25018  2lgslem3  25029  2lgs  25032  dchrvmasum2if  25086  dchrvmasumiflem1  25090  rpvmasum2  25101  pntrlog2bndlem4  25169  pntrlog2bndlem5  25170  padicabv  25219  ostth2lem4  25225  axlowdimlem15  25736  opvtxval  25783  opiedgval  25786  elimifd  29209  elim2if  29210  resvid2  29613  fzto1stfv1  29636  xrge0iifcnv  29761  xrge0iifiso  29763  xrge0iifhom  29765  indval2  29858  ind1  29862  sigaclfu2  29965  ddeval1  30078  eulerpartlemb  30211  ballotlemsima  30358  ballotlemrv1  30363  signsw0glem  30410  signswmnd  30414  signswrid  30415  indispconn  30924  mrsubvr  31116  dfrdg2  31402  dfrdg3  31403  noprefixmo  31573  nosino  31575  unisnif  31674  dfrdg4  31700  fnejoin2  32006  unbdqndv2lem2  32143  bj-xpima2sn  32592  finxpreclem1  32858  finxpreclem3  32862  matunitlindflem1  33037  poimirlem2  33043  poimirlem15  33056  poimirlem16  33057  poimirlem17  33058  poimirlem19  33060  poimirlem20  33061  poimirlem24  33065  mblfinlem2  33079  mbfposadd  33089  itg2addnclem  33093  itg2gt0cn  33097  ibladdnclem  33098  itgaddnclem1  33100  iblabsnclem  33105  iblabsnc  33106  iblmulc2nc  33107  bddiblnc  33112  itggt0cn  33114  ftc1anclem4  33120  ftc1anclem5  33121  ftc1anclem6  33122  ftc1anclem7  33123  ftc1anclem8  33124  ftc1anc  33125  areacirclem5  33136  areacirc  33137  fdc  33173  heiborlem4  33245  ac6s6  33612  cdleme27a  35135  cdleme31sn1  35149  cdleme31fv1  35159  cdlemk40t  35686  dihvalb  36006  pw2f1ocnv  37084  aomclem5  37108  kelac1  37113  sdrgacs  37252  mon1pid  37264  arearect  37282  areaquad  37283  clsk1indlem1  37825  refsum2cnlem1  38679  upbdrech2  38986  lptioo2  39267  lptioo1  39268  limsupmnfuzlem  39362  limsupre3uzlem  39371  coskpi2  39380  cosknegpi  39383  cncfiooicclem1  39410  cncfiooiccre  39412  dvnxpaek  39463  dvnprodlem1  39467  dvnprodlem3  39469  itgioocnicc  39500  iblcncfioo  39501  volico  39507  sublevolico  39508  volioore  39514  voliooico  39516  voliccico  39523  dirkerper  39620  dirkertrigeq  39625  dirkercncflem2  39628  fourierdlem10  39641  fourierdlem32  39663  fourierdlem33  39664  fourierdlem37  39668  fourierdlem62  39692  fourierdlem73  39703  fourierdlem74  39704  fourierdlem75  39705  fourierdlem79  39709  fourierdlem81  39711  fourierdlem82  39712  fourierdlem93  39723  fourierdlem97  39727  fourierdlem101  39731  fourierdlem103  39733  fourierdlem104  39734  sqwvfoura  39752  sqwvfourb  39753  fourierswlem  39754  fouriersw  39755  etransclem4  39762  etransclem15  39773  etransclem19  39777  etransclem20  39778  etransclem23  39781  etransclem24  39782  etransclem25  39783  etransclem27  39785  etransclem31  39789  etransclem32  39790  ioorrnopnxrlem  39833  nnfoctbdjlem  39979  isomenndlem  40051  ovn0val  40071  hoidmv0val  40104  hsphoidmvle2  40106  hoidmv1lelem1  40112  hoidmv1lelem2  40113  hoidmv1le  40115  hoidmvlelem2  40117  hoidmvlelem3  40118  ovnhoilem1  40122  hspdifhsp  40137  hoidifhspdmvle  40141  hspmbllem1  40147  hspmbllem2  40148  hspmbl  40150  volico2  40162  ovnsubadd2lem  40166  ovolval4lem2  40171  ovolval5lem1  40173  afvfundmfveq  40522  pfxccat3a  40728  cshword2  40736  linc1  41502  lincext3  41533  lindslinindsimp1  41534  el0ldep  41543  islindeps2  41560
  Copyright terms: Public domain W3C validator