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

Theorem iftrue 4471
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 1035 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2950 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4467 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2875 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  {cab 2799  ifcif 4465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4466
This theorem is referenced by:  iftruei  4472  iftrued  4473  ifsb  4478  ifbi  4486  ifeq2da  4496  ifeq12da  4497  ifclda  4499  ifeqda  4500  elimif  4501  ifbothda  4502  ifid  4504  ifeqor  4514  ifnot  4515  ifan  4516  ifor  4517  2if2  4518  dedth  4521  elimhyp  4528  elimhyp2v  4529  elimhyp3v  4530  elimhyp4v  4531  elimdhyp  4533  keephyp2v  4535  keephyp3v  4536  dfopif  4794  dfopg  4795  somin1  5987  somincom  5988  xpima1  6034  elimdelov  7239  ovif12  7242  tz7.44-1  8033  resixpfo  8489  boxriin  8493  boxcutc  8494  pw2f1olem  8610  unxpdomlem2  8712  unxpdomlem3  8713  infsupprpr  8957  ordtypelem1  8971  wemaplem2  9000  unwdomg  9037  ixpiunwdom  9044  cantnfp1lem2  9131  cantnfp1lem3  9132  acndom  9466  dfac12lem2  9559  fin23lem14  9744  axcc2lem  9847  pwfseqlem2  10070  uzin  12267  xrmax1  12558  xrmax2  12559  xrmin1  12560  xrmin2  12561  max1ALT  12569  max0sub  12579  ifle  12580  xmulneg1  12652  fzprval  12958  fztpval  12959  modifeq2int  13291  seqf1olem1  13399  seqf1olem2  13400  bcval2  13655  ccatval1  13920  ccatval1OLD  13921  ccatalpha  13937  swrdccat  14087  pfxccat3a  14090  swrdccat3b  14092  repswswrd  14136  cshword  14143  0csh0  14145  ccatco  14187  sgnn  14443  max0add  14660  absmax  14679  sumrblem  15058  fsumcvg  15059  summolem2a  15062  isum  15066  sumss  15071  sumss2  15073  fsumcvg2  15074  fsumser  15077  fsumsplit  15087  sumsplit  15113  prodrblem  15273  fprodcvg  15274  prodmolem2a  15278  zprod  15281  iprod  15282  iprodn0  15284  prodss  15291  fprodsplit  15310  ruclem2  15575  ruclem3  15576  flodddiv4  15754  sadadd2lem2  15789  sadcf  15792  sadc0  15793  sadcp1  15794  sadcaddlem  15796  smupf  15817  smup0  15818  gcd0val  15836  dfgcd2  15884  eucalgf  15917  eucalginv  15918  eucalglt  15919  lcmf0val  15956  phisum  16117  pc0  16181  pcgcd  16204  pcmptcl  16217  pcmpt  16218  pcmpt2  16219  pcprod  16221  fldivp1  16223  prmreclem2  16243  prmreclem4  16245  1arithlem4  16252  vdwlem6  16312  ramtcl2  16337  ramcl2  16342  ramub1lem1  16352  prmop1  16364  fvprmselelfz  16370  fvprmselgcd1  16371  ressid2  16542  xpsfrnel  16825  xpsaddlem  16836  xpsvsca  16840  mreexexd  16909  gsumval1  17883  mgm2nsgrplem2  18024  sgrp2nmndlem2  18029  symgextfve  18478  symgfixfolem1  18497  pmtrmvd  18515  pmtrfinv  18520  pmtrprfval  18546  pmtrprfvalrn  18547  frgpuptinv  18828  frgpup2  18833  frgpup3lem  18834  cyggex  18949  gsumzsplit  18978  gsummpt1n0  19016  dprdfid  19070  dmdprdsplitlem  19090  sdrgacs  19511  abvtrivd  19542  psrlidm  20113  psrridm  20114  mvrf1  20135  mplmonmul  20175  mplcoe1  20176  mplcoe3  20177  mplcoe5  20179  mplmon2  20203  subrgasclcl  20209  evlslem3  20223  evlslem1  20225  coe1tmfv1  20372  ply1sclid  20386  znf1o  20628  uvcvv1  20863  dmatmul  21036  scmatscmiddistr  21047  1mavmul  21087  mulmarep1gsum2  21113  1marepvmarrepid  21114  mdetdiag  21138  mdetralt2  21148  mdetunilem2  21152  mdetunilem7  21157  mdetunilem8  21158  mdetunilem9  21159  mndifsplit  21175  maducoeval2  21179  madugsum  21182  madurid  21183  gsummatr01lem3  21196  gsummatr01  21198  smadiadetglem2  21211  1elcpmat  21253  decpmatid  21308  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  ptpjpre1  22109  ptbasfi  22119  ptpjopn  22150  isfcls  22547  ptcmplem2  22591  ptcmplem3  22592  tsmssplit  22689  dscmet  23111  dscopn  23112  icccmplem2  23360  iccpnfcnv  23477  xrhmeo  23479  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevlem  23559  cmetcaulem  23820  ovolicc1  24046  ioorcl  24107  i1f1lem  24219  itg11  24221  itg1addlem2  24227  itg1addlem4  24229  i1fres  24235  itg1climres  24244  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1flim  24253  itg2const2  24271  itg2seq  24272  itg2uba  24273  itg2splitlem  24278  itg2split  24279  itg2monolem1  24280  itg2cnlem1  24291  itg2cnlem2  24292  iblcnlem  24318  iblss  24334  iblss2  24335  itgitg2  24336  itgle  24339  itgss  24341  itgss2  24342  itgss3  24344  itgless  24346  ibladdlem  24349  itgaddlem1  24352  iblabslem  24357  iblabs  24358  iblabsr  24359  iblmulc2  24360  bddmulibl  24368  itggt0  24371  itgcn  24372  limcvallem  24398  ellimc2  24404  limccnp  24418  limccnp2  24419  limcco  24420  dvcobr  24472  dvexp2  24480  elply2  24715  elplyd  24721  ply1termlem  24722  coe1termlem  24777  abelthlem9  24957  logtayl  25170  leibpilem2  25447  leibpi  25448  rlimcnp2  25472  efrlim  25475  igamz  25553  isnsqf  25640  mule1  25653  sqff1o  25687  muinv  25698  chtublem  25715  dchrelbasd  25743  bposlem1  25788  bposlem3  25790  bposlem5  25792  bposlem6  25793  lgsval2lem  25811  lgsneg  25825  lgsdilem  25828  lgsdir2  25834  lgsdir  25836  lgsdi  25838  lgsne0  25839  gausslemma2dlem1a  25869  2lgslem1c  25897  2lgslem3  25908  2lgs  25911  dchrvmasum2if  26001  dchrvmasumiflem1  26005  rpvmasum2  26016  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  padicabv  26134  ostth2lem4  26140  axlowdimlem15  26670  opvtxval  26716  opiedgval  26719  elimifd  30226  elim2if  30227  ifeq3da  30229  pmtridf1o  30664  fzto1stfv1  30671  resvid2  30829  xrge0iifcnv  31076  xrge0iifiso  31078  xrge0iifhom  31080  indval2  31173  ind1  31176  sigaclfu2  31280  ddeval1  31393  eulerpartlemb  31526  ballotlemsima  31673  ballotlemrv1  31678  signsw0glem  31723  signswmnd  31727  signswrid  31728  indispconn  32379  ex-sategoelel  32566  ex-sategoelelomsuc  32571  ex-sategoelel12  32572  mrsubvr  32656  dfrdg2  32938  dfrdg3  32939  noprefixmo  33100  nosupno  33101  nosupbday  33103  nosupbnd1  33112  nosupbnd2  33114  unisnif  33284  dfrdg4  33310  fnejoin2  33615  unbdqndv2lem2  33747  bj-xpima2sn  34168  finxpreclem1  34553  finxpreclem3  34557  matunitlindflem1  34770  poimirlem2  34776  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  mblfinlem2  34812  mbfposadd  34821  itg2addnclem  34825  itg2gt0cn  34829  ibladdnclem  34830  itgaddnclem1  34832  iblabsnclem  34837  iblabsnc  34838  iblmulc2nc  34839  bddiblnc  34844  itggt0cn  34846  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  areacirclem5  34868  areacirc  34869  fdc  34903  heiborlem4  34975  ac6s6  35333  cdleme27a  37385  cdleme31sn1  37399  cdleme31fv1  37409  cdlemk40t  37936  dihvalb  38255  dffltz  39151  pw2f1ocnv  39514  aomclem5  39538  kelac1  39543  mon1pid  39685  arearect  39702  areaquad  39703  clsk1indlem1  40275  refsum2cnlem1  41174  upbdrech2  41455  lptioo2  41792  lptioo1  41793  limsupmnfuzlem  41887  limsupre3uzlem  41896  limsup10exlem  41933  coskpi2  42027  cosknegpi  42030  cncfiooicclem1  42056  cncfiooiccre  42058  dvnxpaek  42107  dvnprodlem1  42111  dvnprodlem3  42113  itgioocnicc  42142  iblcncfioo  42143  volico  42149  sublevolico  42150  volioore  42156  voliooico  42158  voliccico  42165  dirkerper  42262  dirkertrigeq  42267  dirkercncflem2  42270  fourierdlem10  42283  fourierdlem32  42305  fourierdlem33  42306  fourierdlem37  42310  fourierdlem62  42334  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem93  42365  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem4  42404  etransclem15  42415  etransclem19  42419  etransclem20  42420  etransclem23  42423  etransclem24  42424  etransclem25  42425  etransclem27  42427  etransclem31  42431  etransclem32  42432  ioorrnopnxrlem  42472  nnfoctbdjlem  42618  isomenndlem  42693  ovn0val  42713  hoidmv0val  42746  hsphoidmvle2  42748  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1le  42757  hoidmvlelem2  42759  hoidmvlelem3  42760  ovnhoilem1  42764  hspdifhsp  42779  hoidifhspdmvle  42783  hspmbllem1  42789  hspmbllem2  42790  hspmbl  42792  volico2  42804  ovnsubadd2lem  42808  ovolval4lem2  42813  ovolval5lem1  42815  afvfundmfveq  43218  dfatafv2iota  43290  dfatafv2eqfv  43341  prproropf1olem3  43514  prproropf1olem4  43515  linc1  44378  lincext3  44409  lindslinindsimp1  44410  el0ldep  44419  islindeps2  44436
  Copyright terms: Public domain W3C validator