Theorem iftrue 4479

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.

Step	Hyp	Ref	Expression
1		dfif2 4475	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1043	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	eqabdv 2862	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2784	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2110  {cab 2708  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4474

This theorem is referenced by:  iftruei  4480  iftrued  4481  iftrueb  4486  ifsb  4487  ifbi  4496  ifeq2da  4506  ifeq12da  4507  ifclda  4509  ifeqda  4510  elimif  4511  ifbothda  4512  ifid  4514  ifeqor  4525  ifnot  4526  ifan  4527  ifor  4528  2if2  4529  dedth  4532  elimhyp  4539  elimhyp2v  4540  elimhyp3v  4541  elimhyp4v  4542  elimdhyp  4544  keephyp2v  4546  keephyp3v  4547  dfopif  4820  dfopg  4821  somin1  6077  somincom  6078  xpima1  6127  elimdelov  7437  brif1  7438  ovif12  7441  ifmpt2v  7443  tz7.44-1  8320  rdg0n  8348  resixpfo  8855  boxriin  8859  boxcutc  8860  pw2f1olem  8989  unxpdomlem2  9136  unxpdomlem3  9137  infsupprpr  9385  ordtypelem1  9399  wemaplem2  9428  unwdomg  9465  ixpiunwdom  9471  cantnfp1lem2  9564  cantnfp1lem3  9565  ssttrcl  9600  ttrclselem2  9611  acndom  9934  dfac12lem2  10028  fin23lem14  10216  axcc2lem  10319  pwfseqlem2  10542  uzin  12764  xrmax1  13066  xrmax2  13067  xrmin1  13068  xrmin2  13069  max1ALT  13077  max0sub  13087  ifle  13088  xmulneg1  13160  fzprval  13477  fztpval  13478  modifeq2int  13832  seqf1olem1  13940  seqf1olem2  13941  bcval2  14204  tpf1ofv0  14395  tpf1ofv1  14396  ccatval1  14476  ccatalpha  14493  swrdccat  14634  pfxccat3a  14637  swrdccat3b  14639  repswswrd  14683  cshword  14690  0csh0  14692  ccatco  14734  sgnn  14993  max0add  15209  absmax  15229  sumrblem  15610  fsumcvg  15611  summolem2a  15614  isum  15618  sumss  15623  sumss2  15625  fsumcvg2  15626  fsumser  15629  fsumsplit  15640  sumsplit  15667  prodrblem  15828  fprodcvg  15829  prodmolem2a  15833  zprod  15836  iprod  15837  iprodn0  15839  prodss  15846  fprodsplit  15865  ruclem2  16133  ruclem3  16134  flodddiv4  16318  sadadd2lem2  16353  sadcf  16356  sadc0  16357  sadcp1  16358  sadcaddlem  16360  smupf  16381  smup0  16382  gcd0val  16400  dfgcd2  16449  eucalgf  16486  eucalginv  16487  eucalglt  16488  lcmf0val  16525  phisum  16694  pc0  16758  pcgcd  16782  pcmptcl  16795  pcmpt  16796  pcmpt2  16797  pcprod  16799  fldivp1  16801  prmreclem2  16821  prmreclem4  16823  1arithlem4  16830  vdwlem6  16890  ramtcl2  16915  ramcl2  16920  ramub1lem1  16930  prmop1  16942  fvprmselelfz  16948  fvprmselgcd1  16949  ressid2  17137  xpsfrnel  17458  xpsaddlem  17469  xpsvsca  17473  mreexexd  17546  gsumval1  18583  mgm2nsgrplem2  18819  sgrp2nmndlem2  18824  symgextfve  19324  symgfixfolem1  19343  pmtrmvd  19361  pmtrfinv  19366  pmtrprfval  19392  pmtrprfvalrn  19393  frgpuptinv  19676  frgpup2  19681  frgpup3lem  19682  cyggex  19803  gsumzsplit  19832  gsummpt1n0  19870  dprdfid  19924  dmdprdsplitlem  19944  sdrgacs  20709  abvtrivd  20740  znf1o  21481  uvcvv1  21719  psrlidm  21892  psrridm  21893  mvrf1  21916  mplmonmul  21964  mplcoe1  21965  mplcoe3  21966  mplcoe5  21968  mplmon2  21989  subrgasclcl  21995  evlslem3  22008  evlslem1  22010  psdmul  22074  psdmvr  22077  coe1tmfv1  22181  ply1sclid  22195  dmatmul  22405  scmatscmiddistr  22416  1mavmul  22456  mulmarep1gsum2  22482  1marepvmarrepid  22483  mdetdiag  22507  mdetralt2  22517  mdetunilem2  22521  mdetunilem7  22526  mdetunilem8  22527  mdetunilem9  22528  mndifsplit  22544  maducoeval2  22548  madugsum  22551  madurid  22552  gsummatr01lem3  22565  gsummatr01  22567  smadiadetglem2  22580  1elcpmat  22623  decpmatid  22678  chfacfscmulgsum  22768  chfacfpmmulgsum  22772  ptpjpre1  23479  ptbasfi  23489  ptpjopn  23520  isfcls  23917  ptcmplem2  23961  ptcmplem3  23962  tsmssplit  24060  dscmet  24480  dscopn  24481  icccmplem2  24732  iccpnfcnv  24862  xrhmeo  24864  pcopt  24942  pcopt2  24943  pcoass  24944  pcorevlem  24946  cmetcaulem  25208  ovolicc1  25437  ioorcl  25498  i1f1lem  25610  itg11  25612  itg1addlem2  25618  itg1addlem4  25620  i1fres  25626  itg1climres  25635  mbfi1fseqlem4  25639  mbfi1fseqlem5  25640  mbfi1flim  25644  itg2const2  25662  itg2seq  25663  itg2uba  25664  itg2splitlem  25669  itg2split  25670  itg2monolem1  25671  itg2cnlem1  25682  itg2cnlem2  25683  iblcnlem  25710  iblss  25726  iblss2  25727  itgitg2  25728  itgle  25731  itgss  25733  itgss2  25734  itgss3  25736  itgless  25738  ibladdlem  25741  itgaddlem1  25744  iblabslem  25749  iblabs  25750  iblabsr  25751  iblmulc2  25752  bddmulibl  25760  bddiblnc  25763  itggt0  25765  itgcn  25766  limcvallem  25792  ellimc2  25798  limccnp  25812  limccnp2  25813  limcco  25814  dvcobr  25869  dvcobrOLD  25870  dvexp2  25878  mon1pid  26079  elply2  26121  elplyd  26127  ply1termlem  26128  coe1termlem  26183  abelthlem9  26370  logtayl  26589  leibpilem2  26871  leibpi  26872  rlimcnp2  26896  efrlim  26899  efrlimOLD  26900  igamz  26978  isnsqf  27065  mule1  27078  sqff1o  27112  muinv  27123  chtublem  27142  dchrelbasd  27170  bposlem1  27215  bposlem3  27217  bposlem5  27219  bposlem6  27220  lgsval2lem  27238  lgsneg  27252  lgsdilem  27255  lgsdir2  27261  lgsdir  27263  lgsdi  27265  lgsne0  27266  gausslemma2dlem1a  27296  2lgslem1c  27324  2lgslem3  27335  2lgs  27338  dchrvmasum2if  27428  dchrvmasumiflem1  27432  rpvmasum2  27443  pntrlog2bndlem4  27511  pntrlog2bndlem5  27512  padicabv  27561  ostth2lem4  27567  nosupno  27635  nosupbday  27637  nosupbnd1  27646  nosupbnd2  27648  noinfno  27650  noinfbday  27652  noinfbnd1  27661  maxs1  27697  maxs2  27698  mins1  27699  mins2  27700  abssid  28172  abssge0  28176  axlowdimlem15  28927  opvtxval  28974  opiedgval  28977  elimifd  32513  elim2if  32514  ifeq3da  32516  ifnefals  32518  fmptunsnop  32671  indval2  32825  ind1  32828  pmtridf1o  33053  fzto1stfv1  33060  resvid2  33285  2sqr3minply  33783  cos9thpiminply  33791  xrge0iifcnv  33936  xrge0iifiso  33938  xrge0iifhom  33940  sigaclfu2  34124  ddeval1  34237  eulerpartlemb  34371  ballotlemsima  34519  ballotlemrv1  34524  signsw0glem  34556  signswmnd  34560  signswrid  34561  indispconn  35246  ex-sategoelel  35433  ex-sategoelelomsuc  35438  ex-sategoelel12  35439  mrsubvr  35523  dfrdg2  35808  dfrdg3  35809  unisnif  35938  dfrdg4  35964  fnejoin2  36382  unbdqndv2lem2  36523  bj-xpima2sn  36971  finxpreclem1  37402  finxpreclem3  37406  matunitlindflem1  37635  poimirlem2  37641  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem19  37658  poimirlem20  37659  poimirlem24  37663  mblfinlem2  37677  mbfposadd  37686  itg2addnclem  37690  itg2gt0cn  37694  ibladdnclem  37695  itgaddnclem1  37697  iblabsnclem  37702  iblabsnc  37703  iblmulc2nc  37704  itggt0cn  37709  ftc1anclem4  37715  ftc1anclem5  37716  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  areacirclem5  37731  areacirc  37732  fdc  37764  heiborlem4  37833  ac6s6  38191  cdleme27a  40385  cdleme31sn1  40399  cdleme31fv1  40409  cdlemk40t  40936  dihvalb  41255  sticksstones12a  42169  brif2  42236  brif12  42237  evlsbagval  42578  selvvvval  42597  fsuppind  42602  dffltz  42646  pw2f1ocnv  43049  aomclem5  43070  kelac1  43075  arearect  43227  areaquad  43228  oe0rif  43297  cantnfresb  43336  safesnsupfidom1o  43429  safesnsupfilb  43430  clsk1indlem1  44057  refsum2cnlem1  45053  upbdrech2  45328  lptioo2  45650  lptioo1  45651  limsupmnfuzlem  45743  limsupre3uzlem  45752  limsup10exlem  45789  coskpi2  45883  cosknegpi  45886  cncfiooicclem1  45910  cncfiooiccre  45912  dvnxpaek  45959  dvnprodlem1  45963  dvnprodlem3  45965  itgioocnicc  45994  iblcncfioo  45995  volico  46000  sublevolico  46001  volioore  46007  voliooico  46009  voliccico  46016  dirkerper  46113  dirkertrigeq  46118  dirkercncflem2  46121  fourierdlem10  46134  fourierdlem32  46156  fourierdlem33  46157  fourierdlem37  46161  fourierdlem62  46185  fourierdlem73  46196  fourierdlem74  46197  fourierdlem75  46198  fourierdlem79  46202  fourierdlem81  46204  fourierdlem82  46205  fourierdlem93  46216  fourierdlem97  46220  fourierdlem101  46224  fourierdlem103  46226  fourierdlem104  46227  sqwvfoura  46245  sqwvfourb  46246  fourierswlem  46247  fouriersw  46248  etransclem4  46255  etransclem15  46266  etransclem19  46270  etransclem20  46271  etransclem23  46274  etransclem24  46275  etransclem25  46276  etransclem27  46278  etransclem31  46282  etransclem32  46283  ioorrnopnxrlem  46323  nnfoctbdjlem  46472  isomenndlem  46547  ovn0val  46567  hoidmv0val  46600  hsphoidmvle2  46602  hoidmv1lelem1  46608  hoidmv1lelem2  46609  hoidmv1le  46611  hoidmvlelem2  46613  hoidmvlelem3  46614  ovnhoilem1  46618  hspdifhsp  46633  hoidifhspdmvle  46637  hspmbllem1  46643  hspmbllem2  46644  hspmbl  46646  volico2  46658  ovnsubadd2lem  46662  ovolval4lem2  46667  ovolval5lem1  46669  afvfundmfveq  47148  dfatafv2iota  47220  dfatafv2eqfv  47271  difmodm1lt  47369  prproropf1olem3  47515  prproropf1olem4  47516  linc1  48436  lincext3  48467  lindslinindsimp1  48468  el0ldep  48477  islindeps2  48494  itcoval0  48673  ackval0  48691