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

Theorem iftrue 4296
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 1057 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2937 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4292 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2870 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2157  {cab 2803  ifcif 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-if 4291
This theorem is referenced by:  iftruei  4297  iftrued  4298  ifsb  4303  ifbi  4311  ifeq2da  4321  ifeq12da  4322  ifclda  4324  ifeqda  4325  elimif  4326  ifbothda  4327  ifid  4329  ifeqor  4339  ifnot  4340  ifan  4341  ifor  4342  2if2  4343  dedth  4346  elimhyp  4353  elimhyp2v  4354  elimhyp3v  4355  elimhyp4v  4356  elimdhyp  4358  keephyp2v  4360  keephyp3v  4361  dfopif  4603  dfopg  4604  somin1  5754  somincom  5755  xpima1  5802  dfiota4OLD  6103  elimdelov  6976  ovif12  6979  tz7.44-1  7748  resixpfo  8193  boxriin  8197  boxcutc  8198  pw2f1olem  8313  unxpdomlem2  8414  unxpdomlem3  8415  ordtypelem1  8672  wemaplem2  8701  unwdomg  8738  ixpiunwdom  8745  cantnfp1lem2  8833  cantnfp1lem3  8834  acndom  9167  dfac12lem2  9261  fin23lem14  9450  axcc2lem  9553  pwfseqlem2  9776  uzin  11958  xrmax1  12244  xrmax2  12245  xrmin1  12246  xrmin2  12247  max1ALT  12255  max0sub  12265  ifle  12266  xmulneg1  12337  fzprval  12644  fztpval  12645  modifeq2int  12976  seqf1olem1  13083  seqf1olem2  13084  bcval2  13332  ccatval1  13594  ccatalpha  13610  swrdccat  13737  swrdccat3a  13738  swrdccat3b  13740  repswswrd  13775  cshword  13781  0csh0  13783  ccatco  13825  sgnn  14077  max0add  14293  absmax  14312  sumrblem  14685  fsumcvg  14686  summolem2a  14689  isum  14693  sumss  14698  sumss2  14700  fsumcvg2  14701  fsumser  14704  fsumsplit  14714  sumsplit  14742  prodrblem  14900  fprodcvg  14901  prodmolem2a  14905  zprod  14908  iprod  14909  iprodn0  14911  prodss  14918  fprodsplit  14937  ruclem2  15201  ruclem3  15202  flodddiv4  15376  sadadd2lem2  15411  sadcf  15414  sadc0  15415  sadcp1  15416  sadcaddlem  15418  smupf  15439  smup0  15440  gcd0val  15458  dfgcd2  15502  eucalgf  15535  eucalginv  15536  eucalglt  15537  lcmf0val  15574  phisum  15732  pc0  15796  pcgcd  15819  pcmptcl  15832  pcmpt  15833  pcmpt2  15834  pcprod  15836  fldivp1  15838  prmreclem2  15858  prmreclem4  15860  1arithlem4  15867  vdwlem6  15927  ramtcl2  15952  ramcl2  15957  ramub1lem1  15967  prmop1  15979  fvprmselelfz  15985  fvprmselgcd1  15986  ressid2  16159  xpscfv  16447  xpsfrnel  16448  xpsaddlem  16460  xpsvsca  16464  mreexexd  16533  gsumval1  17502  mgm2nsgrplem2  17631  sgrp2nmndlem2  17636  symgextfve  18060  symgfixfolem1  18079  pmtrmvd  18097  pmtrfinv  18102  pmtrprfval  18128  pmtrprfvalrn  18129  frgpuptinv  18405  frgpup2  18410  frgpup3lem  18411  cyggex  18520  gsumzsplit  18548  gsummpt1n0  18585  dprdfid  18638  dmdprdsplitlem  18658  abvtrivd  19064  psrlidm  19632  psrridm  19633  mvrf1  19654  mplmonmul  19693  mplcoe1  19694  mplcoe3  19695  mplcoe5  19697  mplmon2  19721  subrgasclcl  19727  evlslem3  19742  evlslem1  19743  coe1tmfv1  19872  ply1sclid  19886  znf1o  20127  uvcvv1  20359  dmatmul  20535  scmatscmiddistr  20546  1mavmul  20586  mulmarep1gsum2  20612  1marepvmarrepid  20613  mdetdiag  20637  mdetralt2  20647  mdetunilem2  20651  mdetunilem7  20656  mdetunilem8  20657  mdetunilem9  20658  mndifsplit  20674  maducoeval2  20678  madugsum  20681  madurid  20682  gsummatr01lem3  20696  gsummatr01  20698  smadiadetglem2  20711  1elcpmat  20754  decpmatid  20809  chfacfscmulgsum  20899  chfacfpmmulgsum  20903  ptpjpre1  21609  ptbasfi  21619  ptpjopn  21650  isfcls  22047  ptcmplem2  22091  ptcmplem3  22092  tsmssplit  22189  dscmet  22611  dscopn  22612  icccmplem2  22860  iccpnfcnv  22977  xrhmeo  22979  pcohtpylem  23052  pcopt  23055  pcopt2  23056  pcoass  23057  pcorevlem  23059  cmetcaulem  23320  ovolicc1  23520  ioorcl  23581  i1f1lem  23693  itg11  23695  itg1addlem2  23701  itg1addlem4  23703  i1fres  23709  itg1climres  23718  mbfi1fseqlem4  23722  mbfi1fseqlem5  23723  mbfi1flim  23727  itg2const2  23745  itg2seq  23746  itg2uba  23747  itg2splitlem  23752  itg2split  23753  itg2monolem1  23754  itg2cnlem1  23765  itg2cnlem2  23766  iblcnlem  23792  iblss  23808  iblss2  23809  itgitg2  23810  itgle  23813  itgss  23815  itgss2  23816  itgss3  23818  itgless  23820  ibladdlem  23823  itgaddlem1  23826  iblabslem  23831  iblabs  23832  iblabsr  23833  iblmulc2  23834  bddmulibl  23842  itggt0  23845  itgcn  23846  limcvallem  23872  ellimc2  23878  limccnp  23892  limccnp2  23893  limcco  23894  dvcobr  23946  dvexp2  23954  elply2  24189  elplyd  24195  ply1termlem  24196  coe1termlem  24251  abelthlem9  24431  logtayl  24643  leibpilem2  24905  leibpi  24906  rlimcnp2  24930  efrlim  24933  igamz  25011  isnsqf  25098  mule1  25111  sqff1o  25145  muinv  25156  chtublem  25173  dchrelbasd  25201  bposlem1  25246  bposlem3  25248  bposlem5  25250  bposlem6  25251  lgsval2lem  25269  lgsneg  25283  lgsdilem  25286  lgsdir2  25292  lgsdir  25294  lgsdi  25296  lgsne0  25297  gausslemma2dlem1a  25327  2lgslem1c  25355  2lgslem3  25366  2lgs  25369  dchrvmasum2if  25423  dchrvmasumiflem1  25427  rpvmasum2  25438  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  padicabv  25556  ostth2lem4  25562  axlowdimlem15  26073  opvtxval  26120  opiedgval  26123  elimifd  29710  elim2if  29711  ifeq3da  29713  resvid2  30176  fzto1stfv1  30199  pmtridf1o  30204  xrge0iifcnv  30327  xrge0iifiso  30329  xrge0iifhom  30331  indval2  30424  ind1  30427  sigaclfu2  30532  ddeval1  30645  eulerpartlemb  30778  ballotlemsima  30925  ballotlemrv1  30930  signsw0glem  30978  signswmnd  30982  signswrid  30983  indispconn  31561  mrsubvr  31753  dfrdg2  32043  dfrdg3  32044  noprefixmo  32191  nosupno  32192  nosupbday  32194  nosupbnd1  32203  nosupbnd2  32205  unisnif  32375  dfrdg4  32401  fnejoin2  32707  unbdqndv2lem2  32840  bj-xpima2sn  33274  finxpreclem1  33561  finxpreclem3  33565  matunitlindflem1  33737  poimirlem2  33743  poimirlem15  33756  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem24  33765  mblfinlem2  33779  mbfposadd  33788  itg2addnclem  33792  itg2gt0cn  33796  ibladdnclem  33797  itgaddnclem1  33799  iblabsnclem  33804  iblabsnc  33805  iblmulc2nc  33806  bddiblnc  33811  itggt0cn  33813  ftc1anclem4  33819  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  areacirclem5  33835  areacirc  33836  fdc  33871  heiborlem4  33943  ac6s6  34309  cdleme27a  36166  cdleme31sn1  36180  cdleme31fv1  36190  cdlemk40t  36717  dihvalb  37036  pw2f1ocnv  38123  aomclem5  38147  kelac1  38152  sdrgacs  38290  mon1pid  38302  arearect  38319  areaquad  38320  clsk1indlem1  38861  refsum2cnlem1  39708  upbdrech2  40021  lptioo2  40361  lptioo1  40362  limsupmnfuzlem  40456  limsupre3uzlem  40465  limsup10exlem  40502  coskpi2  40575  cosknegpi  40578  cncfiooicclem1  40604  cncfiooiccre  40606  dvnxpaek  40655  dvnprodlem1  40659  dvnprodlem3  40661  itgioocnicc  40690  iblcncfioo  40691  volico  40697  sublevolico  40698  volioore  40704  voliooico  40706  voliccico  40713  dirkerper  40810  dirkertrigeq  40815  dirkercncflem2  40818  fourierdlem10  40831  fourierdlem32  40853  fourierdlem33  40854  fourierdlem37  40858  fourierdlem62  40882  fourierdlem73  40893  fourierdlem74  40894  fourierdlem75  40895  fourierdlem79  40899  fourierdlem81  40901  fourierdlem82  40902  fourierdlem93  40913  fourierdlem97  40917  fourierdlem101  40921  fourierdlem103  40923  fourierdlem104  40924  sqwvfoura  40942  sqwvfourb  40943  fourierswlem  40944  fouriersw  40945  etransclem4  40952  etransclem15  40963  etransclem19  40967  etransclem20  40968  etransclem23  40971  etransclem24  40972  etransclem25  40973  etransclem27  40975  etransclem31  40979  etransclem32  40980  ioorrnopnxrlem  41023  nnfoctbdjlem  41169  isomenndlem  41244  ovn0val  41264  hoidmv0val  41297  hsphoidmvle2  41299  hoidmv1lelem1  41305  hoidmv1lelem2  41306  hoidmv1le  41308  hoidmvlelem2  41310  hoidmvlelem3  41311  ovnhoilem1  41315  hspdifhsp  41330  hoidifhspdmvle  41334  hspmbllem1  41340  hspmbllem2  41341  hspmbl  41343  volico2  41355  ovnsubadd2lem  41359  ovolval4lem2  41364  ovolval5lem1  41366  afvfundmfveq  41745  dfatafv2iota  41817  dfatafv2eqfv  41868  pfxccat3a  42022  cshword2  42030  linc1  42800  lincext3  42831  lindslinindsimp1  42832  el0ldep  42841  islindeps2  42858
  Copyright terms: Public domain W3C validator