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

Theorem iftrue 4469
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 2947 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4465 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2872 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  {cab 2796  ifcif 4463
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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-if 4464
This theorem is referenced by:  iftruei  4470  iftrued  4471  ifsb  4476  ifbi  4484  ifeq2da  4494  ifeq12da  4495  ifclda  4497  ifeqda  4498  elimif  4499  ifbothda  4500  ifid  4502  ifeqor  4512  ifnot  4513  ifan  4514  ifor  4515  2if2  4516  dedth  4519  elimhyp  4526  elimhyp2v  4527  elimhyp3v  4528  elimhyp4v  4529  elimdhyp  4531  keephyp2v  4533  keephyp3v  4534  dfopif  4792  dfopg  4793  somin1  5986  somincom  5987  xpima1  6033  elimdelov  7239  ovif12  7242  tz7.44-1  8031  resixpfo  8488  boxriin  8492  boxcutc  8493  pw2f1olem  8609  unxpdomlem2  8711  unxpdomlem3  8712  infsupprpr  8956  ordtypelem1  8970  wemaplem2  8999  unwdomg  9036  ixpiunwdom  9043  cantnfp1lem2  9130  cantnfp1lem3  9131  acndom  9465  dfac12lem2  9558  fin23lem14  9743  axcc2lem  9846  pwfseqlem2  10069  uzin  12266  xrmax1  12556  xrmax2  12557  xrmin1  12558  xrmin2  12559  max1ALT  12567  max0sub  12577  ifle  12578  xmulneg1  12650  fzprval  12956  fztpval  12957  modifeq2int  13289  seqf1olem1  13397  seqf1olem2  13398  bcval2  13653  ccatval1  13918  ccatval1OLD  13919  ccatalpha  13935  swrdccat  14085  pfxccat3a  14088  swrdccat3b  14090  repswswrd  14134  cshword  14141  0csh0  14143  ccatco  14185  sgnn  14441  max0add  14658  absmax  14677  sumrblem  15056  fsumcvg  15057  summolem2a  15060  isum  15064  sumss  15069  sumss2  15071  fsumcvg2  15072  fsumser  15075  fsumsplit  15085  sumsplit  15111  prodrblem  15271  fprodcvg  15272  prodmolem2a  15276  zprod  15279  iprod  15280  iprodn0  15282  prodss  15289  fprodsplit  15308  ruclem2  15573  ruclem3  15574  flodddiv4  15752  sadadd2lem2  15787  sadcf  15790  sadc0  15791  sadcp1  15792  sadcaddlem  15794  smupf  15815  smup0  15816  gcd0val  15834  dfgcd2  15882  eucalgf  15915  eucalginv  15916  eucalglt  15917  lcmf0val  15954  phisum  16115  pc0  16179  pcgcd  16202  pcmptcl  16215  pcmpt  16216  pcmpt2  16217  pcprod  16219  fldivp1  16221  prmreclem2  16241  prmreclem4  16243  1arithlem4  16250  vdwlem6  16310  ramtcl2  16335  ramcl2  16340  ramub1lem1  16350  prmop1  16362  fvprmselelfz  16368  fvprmselgcd1  16369  ressid2  16540  xpsfrnel  16823  xpsaddlem  16834  xpsvsca  16838  mreexexd  16907  gsumval1  17881  mgm2nsgrplem2  18022  sgrp2nmndlem2  18027  symgextfve  18476  symgfixfolem1  18495  pmtrmvd  18513  pmtrfinv  18518  pmtrprfval  18544  pmtrprfvalrn  18545  frgpuptinv  18826  frgpup2  18831  frgpup3lem  18832  cyggex  18947  gsumzsplit  18976  gsummpt1n0  19014  dprdfid  19068  dmdprdsplitlem  19088  sdrgacs  19509  abvtrivd  19540  psrlidm  20111  psrridm  20112  mvrf1  20133  mplmonmul  20173  mplcoe1  20174  mplcoe3  20175  mplcoe5  20177  mplmon2  20201  subrgasclcl  20207  evlslem3  20221  evlslem1  20223  coe1tmfv1  20370  ply1sclid  20384  znf1o  20626  uvcvv1  20861  dmatmul  21034  scmatscmiddistr  21045  1mavmul  21085  mulmarep1gsum2  21111  1marepvmarrepid  21112  mdetdiag  21136  mdetralt2  21146  mdetunilem2  21150  mdetunilem7  21155  mdetunilem8  21156  mdetunilem9  21157  mndifsplit  21173  maducoeval2  21177  madugsum  21180  madurid  21181  gsummatr01lem3  21194  gsummatr01  21196  smadiadetglem2  21209  1elcpmat  21251  decpmatid  21306  chfacfscmulgsum  21396  chfacfpmmulgsum  21400  ptpjpre1  22107  ptbasfi  22117  ptpjopn  22148  isfcls  22545  ptcmplem2  22589  ptcmplem3  22590  tsmssplit  22687  dscmet  23109  dscopn  23110  icccmplem2  23358  iccpnfcnv  23475  xrhmeo  23477  pcopt  23553  pcopt2  23554  pcoass  23555  pcorevlem  23557  cmetcaulem  23818  ovolicc1  24044  ioorcl  24105  i1f1lem  24217  itg11  24219  itg1addlem2  24225  itg1addlem4  24227  i1fres  24233  itg1climres  24242  mbfi1fseqlem4  24246  mbfi1fseqlem5  24247  mbfi1flim  24251  itg2const2  24269  itg2seq  24270  itg2uba  24271  itg2splitlem  24276  itg2split  24277  itg2monolem1  24278  itg2cnlem1  24289  itg2cnlem2  24290  iblcnlem  24316  iblss  24332  iblss2  24333  itgitg2  24334  itgle  24337  itgss  24339  itgss2  24340  itgss3  24342  itgless  24344  ibladdlem  24347  itgaddlem1  24350  iblabslem  24355  iblabs  24356  iblabsr  24357  iblmulc2  24358  bddmulibl  24366  itggt0  24369  itgcn  24370  limcvallem  24396  ellimc2  24402  limccnp  24416  limccnp2  24417  limcco  24418  dvcobr  24470  dvexp2  24478  elply2  24713  elplyd  24719  ply1termlem  24720  coe1termlem  24775  abelthlem9  24955  logtayl  25170  leibpilem2  25446  leibpi  25447  rlimcnp2  25471  efrlim  25474  igamz  25552  isnsqf  25639  mule1  25652  sqff1o  25686  muinv  25697  chtublem  25714  dchrelbasd  25742  bposlem1  25787  bposlem3  25789  bposlem5  25791  bposlem6  25792  lgsval2lem  25810  lgsneg  25824  lgsdilem  25827  lgsdir2  25833  lgsdir  25835  lgsdi  25837  lgsne0  25838  gausslemma2dlem1a  25868  2lgslem1c  25896  2lgslem3  25907  2lgs  25910  dchrvmasum2if  26000  dchrvmasumiflem1  26004  rpvmasum2  26015  pntrlog2bndlem4  26083  pntrlog2bndlem5  26084  padicabv  26133  ostth2lem4  26139  axlowdimlem15  26669  opvtxval  26715  opiedgval  26718  elimifd  30225  elim2if  30226  ifeq3da  30228  pmtridf1o  30663  fzto1stfv1  30670  resvid2  30828  xrge0iifcnv  31075  xrge0iifiso  31077  xrge0iifhom  31079  indval2  31172  ind1  31175  sigaclfu2  31279  ddeval1  31392  eulerpartlemb  31525  ballotlemsima  31672  ballotlemrv1  31677  signsw0glem  31722  signswmnd  31726  signswrid  31727  indispconn  32378  ex-sategoelel  32565  ex-sategoelelomsuc  32570  ex-sategoelel12  32571  mrsubvr  32655  dfrdg2  32937  dfrdg3  32938  noprefixmo  33099  nosupno  33100  nosupbday  33102  nosupbnd1  33111  nosupbnd2  33113  unisnif  33283  dfrdg4  33309  fnejoin2  33614  unbdqndv2lem2  33746  bj-xpima2sn  34167  finxpreclem1  34552  finxpreclem3  34556  matunitlindflem1  34769  poimirlem2  34775  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem24  34797  mblfinlem2  34811  mbfposadd  34820  itg2addnclem  34824  itg2gt0cn  34828  ibladdnclem  34829  itgaddnclem1  34831  iblabsnclem  34836  iblabsnc  34837  iblmulc2nc  34838  bddiblnc  34843  itggt0cn  34845  ftc1anclem4  34851  ftc1anclem5  34852  ftc1anclem6  34853  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  areacirclem5  34867  areacirc  34868  fdc  34901  heiborlem4  34973  ac6s6  35331  cdleme27a  37383  cdleme31sn1  37397  cdleme31fv1  37407  cdlemk40t  37934  dihvalb  38253  dffltz  39149  pw2f1ocnv  39512  aomclem5  39536  kelac1  39541  mon1pid  39683  arearect  39700  areaquad  39701  clsk1indlem1  40273  refsum2cnlem1  41171  upbdrech2  41451  lptioo2  41788  lptioo1  41789  limsupmnfuzlem  41883  limsupre3uzlem  41892  limsup10exlem  41929  coskpi2  42023  cosknegpi  42026  cncfiooicclem1  42052  cncfiooiccre  42054  dvnxpaek  42103  dvnprodlem1  42107  dvnprodlem3  42109  itgioocnicc  42138  iblcncfioo  42139  volico  42145  sublevolico  42146  volioore  42152  voliooico  42154  voliccico  42161  dirkerper  42258  dirkertrigeq  42263  dirkercncflem2  42266  fourierdlem10  42279  fourierdlem32  42301  fourierdlem33  42302  fourierdlem37  42306  fourierdlem62  42330  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem79  42347  fourierdlem81  42349  fourierdlem82  42350  fourierdlem93  42361  fourierdlem97  42365  fourierdlem101  42369  fourierdlem103  42371  fourierdlem104  42372  sqwvfoura  42390  sqwvfourb  42391  fourierswlem  42392  fouriersw  42393  etransclem4  42400  etransclem15  42411  etransclem19  42415  etransclem20  42416  etransclem23  42419  etransclem24  42420  etransclem25  42421  etransclem27  42423  etransclem31  42427  etransclem32  42428  ioorrnopnxrlem  42468  nnfoctbdjlem  42614  isomenndlem  42689  ovn0val  42709  hoidmv0val  42742  hsphoidmvle2  42744  hoidmv1lelem1  42750  hoidmv1lelem2  42751  hoidmv1le  42753  hoidmvlelem2  42755  hoidmvlelem3  42756  ovnhoilem1  42760  hspdifhsp  42775  hoidifhspdmvle  42779  hspmbllem1  42785  hspmbllem2  42786  hspmbl  42788  volico2  42800  ovnsubadd2lem  42804  ovolval4lem2  42809  ovolval5lem1  42811  afvfundmfveq  43214  dfatafv2iota  43286  dfatafv2eqfv  43337  prproropf1olem3  43544  prproropf1olem4  43545  linc1  44408  lincext3  44439  lindslinindsimp1  44440  el0ldep  44449  islindeps2  44466
  Copyright terms: Public domain W3C validator