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

Theorem iftrue 4475
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 1037 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2954 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4471 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2879 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2106  {cab 2802  ifcif 4469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-if 4470
This theorem is referenced by:  iftruei  4476  iftrued  4477  ifsb  4482  ifbi  4490  ifeq2da  4500  ifeq12da  4501  ifclda  4503  ifeqda  4504  elimif  4505  ifbothda  4506  ifid  4508  ifeqor  4518  ifnot  4519  ifan  4520  ifor  4521  2if2  4522  dedth  4525  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elimdhyp  4537  keephyp2v  4539  keephyp3v  4540  dfopif  4798  dfopg  4799  somin1  5990  somincom  5991  xpima1  6037  elimdelov  7243  ovif12  7246  tz7.44-1  8036  resixpfo  8492  boxriin  8496  boxcutc  8497  pw2f1olem  8613  unxpdomlem2  8715  unxpdomlem3  8716  infsupprpr  8960  ordtypelem1  8974  wemaplem2  9003  unwdomg  9040  ixpiunwdom  9047  cantnfp1lem2  9134  cantnfp1lem3  9135  acndom  9469  dfac12lem2  9562  fin23lem14  9747  axcc2lem  9850  pwfseqlem2  10073  uzin  12270  xrmax1  12561  xrmax2  12562  xrmin1  12563  xrmin2  12564  max1ALT  12572  max0sub  12582  ifle  12583  xmulneg1  12655  fzprval  12961  fztpval  12962  modifeq2int  13294  seqf1olem1  13402  seqf1olem2  13403  bcval2  13658  ccatval1  13923  ccatval1OLD  13924  ccatalpha  13940  swrdccat  14090  pfxccat3a  14093  swrdccat3b  14095  repswswrd  14139  cshword  14146  0csh0  14148  ccatco  14190  sgnn  14446  max0add  14663  absmax  14682  sumrblem  15060  fsumcvg  15061  summolem2a  15064  isum  15068  sumss  15073  sumss2  15075  fsumcvg2  15076  fsumser  15079  fsumsplit  15089  sumsplit  15115  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  iprod  15284  iprodn0  15286  prodss  15293  fprodsplit  15312  ruclem2  15577  ruclem3  15578  flodddiv4  15756  sadadd2lem2  15791  sadcf  15794  sadc0  15795  sadcp1  15796  sadcaddlem  15798  smupf  15819  smup0  15820  gcd0val  15838  dfgcd2  15886  eucalgf  15919  eucalginv  15920  eucalglt  15921  lcmf0val  15958  phisum  16119  pc0  16183  pcgcd  16206  pcmptcl  16219  pcmpt  16220  pcmpt2  16221  pcprod  16223  fldivp1  16225  prmreclem2  16245  prmreclem4  16247  1arithlem4  16254  vdwlem6  16314  ramtcl2  16339  ramcl2  16344  ramub1lem1  16354  prmop1  16366  fvprmselelfz  16372  fvprmselgcd1  16373  ressid2  16544  xpsfrnel  16827  xpsaddlem  16838  xpsvsca  16842  mreexexd  16911  gsumval1  17884  mgm2nsgrplem2  18019  sgrp2nmndlem2  18024  symgextfve  18469  symgfixfolem1  18488  pmtrmvd  18506  pmtrfinv  18511  pmtrprfval  18537  pmtrprfvalrn  18538  frgpuptinv  18819  frgpup2  18824  frgpup3lem  18825  cyggex  18940  gsumzsplit  18969  gsummpt1n0  19007  dprdfid  19061  dmdprdsplitlem  19081  sdrgacs  19502  abvtrivd  19533  psrlidm  20104  psrridm  20105  mvrf1  20126  mplmonmul  20165  mplcoe1  20166  mplcoe3  20167  mplcoe5  20169  mplmon2  20193  subrgasclcl  20199  evlslem3  20213  evlslem1  20215  coe1tmfv1  20359  ply1sclid  20373  znf1o  20614  uvcvv1  20849  dmatmul  21022  scmatscmiddistr  21033  1mavmul  21073  mulmarep1gsum2  21099  1marepvmarrepid  21100  mdetdiag  21124  mdetralt2  21134  mdetunilem2  21138  mdetunilem7  21143  mdetunilem8  21144  mdetunilem9  21145  mndifsplit  21161  maducoeval2  21165  madugsum  21168  madurid  21169  gsummatr01lem3  21182  gsummatr01  21184  smadiadetglem2  21197  1elcpmat  21239  decpmatid  21294  chfacfscmulgsum  21384  chfacfpmmulgsum  21388  ptpjpre1  22095  ptbasfi  22105  ptpjopn  22136  isfcls  22533  ptcmplem2  22577  ptcmplem3  22578  tsmssplit  22675  dscmet  23097  dscopn  23098  icccmplem2  23346  iccpnfcnv  23463  xrhmeo  23465  pcopt  23541  pcopt2  23542  pcoass  23543  pcorevlem  23545  cmetcaulem  23806  ovolicc1  24032  ioorcl  24093  i1f1lem  24205  itg11  24207  itg1addlem2  24213  itg1addlem4  24215  i1fres  24221  itg1climres  24230  mbfi1fseqlem4  24234  mbfi1fseqlem5  24235  mbfi1flim  24239  itg2const2  24257  itg2seq  24258  itg2uba  24259  itg2splitlem  24264  itg2split  24265  itg2monolem1  24266  itg2cnlem1  24277  itg2cnlem2  24278  iblcnlem  24304  iblss  24320  iblss2  24321  itgitg2  24322  itgle  24325  itgss  24327  itgss2  24328  itgss3  24330  itgless  24332  ibladdlem  24335  itgaddlem1  24338  iblabslem  24343  iblabs  24344  iblabsr  24345  iblmulc2  24346  bddmulibl  24354  itggt0  24357  itgcn  24358  limcvallem  24384  ellimc2  24390  limccnp  24404  limccnp2  24405  limcco  24406  dvcobr  24458  dvexp2  24466  elply2  24701  elplyd  24707  ply1termlem  24708  coe1termlem  24763  abelthlem9  24943  logtayl  25156  leibpilem2  25433  leibpi  25434  rlimcnp2  25458  efrlim  25461  igamz  25539  isnsqf  25626  mule1  25639  sqff1o  25673  muinv  25684  chtublem  25701  dchrelbasd  25729  bposlem1  25774  bposlem3  25776  bposlem5  25778  bposlem6  25779  lgsval2lem  25797  lgsneg  25811  lgsdilem  25814  lgsdir2  25820  lgsdir  25822  lgsdi  25824  lgsne0  25825  gausslemma2dlem1a  25855  2lgslem1c  25883  2lgslem3  25894  2lgs  25897  dchrvmasum2if  25987  dchrvmasumiflem1  25991  rpvmasum2  26002  pntrlog2bndlem4  26070  pntrlog2bndlem5  26071  padicabv  26120  ostth2lem4  26126  axlowdimlem15  26657  opvtxval  26703  opiedgval  26706  elimifd  30213  elim2if  30214  ifeq3da  30216  pmtridf1o  30651  fzto1stfv1  30658  resvid2  30816  xrge0iifcnv  31063  xrge0iifiso  31065  xrge0iifhom  31067  indval2  31160  ind1  31163  sigaclfu2  31267  ddeval1  31380  eulerpartlemb  31513  ballotlemsima  31660  ballotlemrv1  31665  signsw0glem  31710  signswmnd  31714  signswrid  31715  indispconn  32366  ex-sategoelel  32553  ex-sategoelelomsuc  32558  ex-sategoelel12  32559  mrsubvr  32643  dfrdg2  32925  dfrdg3  32926  noprefixmo  33087  nosupno  33088  nosupbday  33090  nosupbnd1  33099  nosupbnd2  33101  unisnif  33271  dfrdg4  33297  fnejoin2  33602  unbdqndv2lem2  33734  bj-xpima2sn  34155  finxpreclem1  34540  finxpreclem3  34544  matunitlindflem1  34756  poimirlem2  34762  poimirlem15  34775  poimirlem16  34776  poimirlem17  34777  poimirlem19  34779  poimirlem20  34780  poimirlem24  34784  mblfinlem2  34798  mbfposadd  34807  itg2addnclem  34811  itg2gt0cn  34815  ibladdnclem  34816  itgaddnclem1  34818  iblabsnclem  34823  iblabsnc  34824  iblmulc2nc  34825  bddiblnc  34830  itggt0cn  34832  ftc1anclem4  34838  ftc1anclem5  34839  ftc1anclem6  34840  ftc1anclem7  34841  ftc1anclem8  34842  ftc1anc  34843  areacirclem5  34854  areacirc  34855  fdc  34889  heiborlem4  34961  ac6s6  35319  cdleme27a  37371  cdleme31sn1  37385  cdleme31fv1  37395  cdlemk40t  37922  dihvalb  38241  dffltz  39133  pw2f1ocnv  39496  aomclem5  39520  kelac1  39525  mon1pid  39667  arearect  39684  areaquad  39685  clsk1indlem1  40257  refsum2cnlem1  41156  upbdrech2  41437  lptioo2  41774  lptioo1  41775  limsupmnfuzlem  41869  limsupre3uzlem  41878  limsup10exlem  41915  coskpi2  42009  cosknegpi  42012  cncfiooicclem1  42038  cncfiooiccre  42040  dvnxpaek  42089  dvnprodlem1  42093  dvnprodlem3  42095  itgioocnicc  42124  iblcncfioo  42125  volico  42131  sublevolico  42132  volioore  42138  voliooico  42140  voliccico  42147  dirkerper  42244  dirkertrigeq  42249  dirkercncflem2  42252  fourierdlem10  42265  fourierdlem32  42287  fourierdlem33  42288  fourierdlem37  42292  fourierdlem62  42316  fourierdlem73  42327  fourierdlem74  42328  fourierdlem75  42329  fourierdlem79  42333  fourierdlem81  42335  fourierdlem82  42336  fourierdlem93  42347  fourierdlem97  42351  fourierdlem101  42355  fourierdlem103  42357  fourierdlem104  42358  sqwvfoura  42376  sqwvfourb  42377  fourierswlem  42378  fouriersw  42379  etransclem4  42386  etransclem15  42397  etransclem19  42401  etransclem20  42402  etransclem23  42405  etransclem24  42406  etransclem25  42407  etransclem27  42409  etransclem31  42413  etransclem32  42414  ioorrnopnxrlem  42454  nnfoctbdjlem  42600  isomenndlem  42675  ovn0val  42695  hoidmv0val  42728  hsphoidmvle2  42730  hoidmv1lelem1  42736  hoidmv1lelem2  42737  hoidmv1le  42739  hoidmvlelem2  42741  hoidmvlelem3  42742  ovnhoilem1  42746  hspdifhsp  42761  hoidifhspdmvle  42765  hspmbllem1  42771  hspmbllem2  42772  hspmbl  42774  volico2  42786  ovnsubadd2lem  42790  ovolval4lem2  42795  ovolval5lem1  42797  afvfundmfveq  43200  dfatafv2iota  43272  dfatafv2eqfv  43323  prproropf1olem3  43496  prproropf1olem4  43497  linc1  44309  lincext3  44340  lindslinindsimp1  44341  el0ldep  44350  islindeps2  44367
  Copyright terms: Public domain W3C validator