Theorem iftrue 4487

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 4483	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1059	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	eqabdv 2893	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2814	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  iftruei  4488  iftrued  4489  iftrueb  4494  ifsb  4495  ifbi  4504  ifeq2da  4514  ifeq12da  4515  ifclda  4517  ifeqda  4518  elimif  4519  ifbothda  4520  ifid  4522  ifeqor  4533  ifnot  4534  ifan  4535  ifor  4536  2if2  4537  dedth  4540  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  dfopif  4829  dfopg  4830  somin1  6121  somincom  6122  xpima1  6170  elimdelov  7504  brif1  7505  ovif12  7508  ifmpt2v  7510  tz7.44-1  8392  rdg0n  8420  resixpfo  8942  boxriin  8946  boxcutc  8947  pw2f1olem  9078  unxpdomlem2  9226  unxpdomlem3  9227  infsupprpr  9476  ordtypelem1  9490  wemaplem2  9519  unwdomg  9556  ixpiunwdom  9562  cantnfp1lem2  9658  cantnfp1lem3  9659  ssttrcl  9694  ttrclselem2  9705  acndom  10102  dfac12lem2  10195  fin23lem14  10383  axcc2lem  10486  pwfseqlem2  10716  indval2  12295  ind1  12299  uzin  12971  xrmax1  13275  xrmax2  13276  xrmin1  13277  xrmin2  13278  max1ALT  13286  max0sub  13296  ifle  13297  xmulneg1  13369  fzprval  13688  fztpval  13689  modifeq2int  14045  seqf1olem1  14153  seqf1olem2  14154  bcval2  14417  tpf1ofv0  14609  tpf1ofv1  14610  ccatval1  14690  ccatalpha  14708  swrdccat  14852  pfxccat3a  14855  swrdccat3b  14857  repswswrd  14903  cshword  14910  0csh0  14912  ccatco  14954  sgnn  15215  max0add  15445  absmax  15465  sumrblem  15845  fsumcvg  15846  summolem2a  15849  isum  15853  sumss  15858  sumss2  15860  fsumcvg2  15861  fsumser  15864  fsumsplit  15875  sumsplit  15902  prodrblem  16064  fprodcvg  16065  prodmolem2a  16069  zprod  16072  iprod  16073  iprodn0  16075  prodss  16082  fprodsplit  16101  ruclem2  16368  ruclem3  16369  flodddiv4  16553  sadadd2lem2  16588  sadcf  16591  sadc0  16592  sadcp1  16593  sadcaddlem  16595  smupf  16616  smup0  16617  gcd0val  16635  dfgcd2  16684  eucalgf  16721  eucalginv  16722  eucalglt  16723  lcmf0val  16760  phisum  16930  pc0  16994  pcgcd  17018  pcmptcl  17031  pcmpt  17032  pcmpt2  17033  pcprod  17035  fldivp1  17037  prmreclem2  17057  prmreclem4  17059  1arithlem4  17066  vdwlem6  17126  ramtcl2  17151  ramcl2  17156  ramub1lem1  17166  prmop1  17178  fvprmselelfz  17184  fvprmselgcd1  17185  ressid2  17374  xpsfrnel  17696  xpsaddlem  17707  xpsvsca  17711  mreexexd  17784  gsumval1  18834  mgm2nsgrplem2  19080  sgrp2nmndlem2  19085  symgextfve  19595  symgfixfolem1  19614  pmtrmvd  19632  pmtrfinv  19637  pmtrprfval  19663  pmtrprfvalrn  19664  frgpuptinv  19947  frgpup2  19952  frgpup3lem  19953  cyggex  20074  gsumzsplit  20103  gsummpt1n0  20141  dprdfid  20195  dmdprdsplitlem  20215  sdrgacs  21020  abvtrivd  21051  znf1o  21819  uvcvv1  22057  psrlidm  22231  psrridm  22232  mvrf1  22255  mplmonmul  22307  mplcoe1  22308  mplcoe3  22309  mplcoe5  22311  mplmon2  22332  subrgasclcl  22338  evlslem3  22351  evlslem1  22353  selvvvval  22413  psdmul  22449  psdmvr  22452  coe1tmfv1  22555  ply1sclid  22569  dmatmul  22774  scmatscmiddistr  22785  1mavmul  22825  mulmarep1gsum2  22851  1marepvmarrepid  22852  mdetdiag  22876  mdetralt2  22886  mdetunilem2  22890  mdetunilem7  22895  mdetunilem8  22896  mdetunilem9  22897  mndifsplit  22913  maducoeval2  22917  madugsum  22920  madurid  22921  gsummatr01lem3  22934  gsummatr01  22936  smadiadetglem2  22949  matunitlindflem1  22956  1elcpmat  22995  decpmatid  23050  chfacfscmulgsum  23140  chfacfpmmulgsum  23144  ptpjpre1  23852  ptbasfi  23862  ptpjopn  23893  isfcls  24290  ptcmplem2  24334  ptcmplem3  24335  tsmssplit  24433  dscmet  24853  dscopn  24854  icccmplem2  25105  iccpnfcnv  25227  xrhmeo  25229  pcopt  25305  pcopt2  25306  pcoass  25307  pcorevlem  25309  cmetcaulem  25571  ovolicc1  25799  ioorcl  25860  i1f1lem  25972  itg11  25974  itg1addlem2  25980  itg1addlem4  25982  i1fres  25988  itg1climres  25997  mbfi1fseqlem4  26001  mbfi1fseqlem5  26002  mbfi1flim  26006  itg2const2  26024  itg2seq  26025  itg2uba  26026  itg2splitlem  26031  itg2split  26032  itg2monolem1  26033  itg2cnlem1  26044  itg2cnlem2  26045  iblcnlem  26071  iblss  26087  iblss2  26088  itgitg2  26089  itgle  26092  itgss  26094  itgss2  26095  itgss3  26097  itgless  26099  ibladdlem  26102  itgaddlem1  26105  iblabslem  26110  iblabs  26111  iblabsr  26112  iblmulc2  26113  bddmulibl  26121  bddiblnc  26124  itggt0  26126  itgcn  26127  limcvallem  26153  ellimc2  26159  limccnp  26173  limccnp2  26174  limcco  26175  dvcobr  26228  dvexp2  26236  mon1pid  26434  elply2  26476  elplyd  26482  ply1termlem  26483  coe1termlem  26539  abelthlem9  26731  logtayl  26952  leibpilem2  27233  leibpi  27234  rlimcnp2  27258  efrlim  27261  igamz  27339  isnsqf  27426  mule1  27439  sqff1o  27473  muinv  27484  chtublem  27502  dchrelbasd  27530  bposlem1  27575  bposlem3  27577  bposlem5  27579  bposlem6  27580  lgsval2lem  27598  lgsneg  27612  lgsdilem  27615  lgsdir2  27621  lgsdir  27623  lgsdi  27625  lgsne0  27626  gausslemma2dlem1a  27656  2lgslem1c  27684  2lgslem3  27695  2lgs  27698  dchrvmasum2if  27788  dchrvmasumiflem1  27792  rpvmasum2  27803  pntrlog2bndlem4  27871  pntrlog2bndlem5  27872  padicabv  27921  ostth2lem4  27927  nosupno  27994  nosupbday  27996  nosupbnd1  28005  nosupbnd2  28007  noinfno  28009  noinfbday  28011  noinfbnd1  28020  maxs1  28060  maxs2  28061  mins1  28062  mins2  28063  abssid  28561  abssge0  28565  axlowdimlem15  29468  opvtxval  29515  opiedgval  29518  elimifd  33073  elim2if  33074  ifeq3da  33076  ifnefals  33078  fmptunsnop  33227  pmtridf1o  33589  fzto1stfv1  33596  resvid2  33825  psrmonmul  34116  vieta  34146  2sqr3minply  34346  cos9thpiminply  34354  xrge0iifcnv  34499  xrge0iifiso  34501  xrge0iifhom  34503  sigaclfu2  34687  ddeval1  34801  eulerpartlemb  34935  ballotlemsima  35083  ballotlemrv1  35088  signsw0glem  35117  signswmnd  35121  signswrid  35122  vonf1oonfo  35819  indispconn  35920  ex-sategoelel  36107  ex-sategoelelomsuc  36112  ex-sategoelel12  36113  mrsubvr  36197  dfrdg2  36479  dfrdg3  36480  unisnif  36609  dfrdg4  36637  fnejoin2  37079  unbdqndv2lem2  37298  bj-xpima2sn  37793  finxpreclem1  38232  finxpreclem3  38236  poimirlem2  38460  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem24  38482  mblfinlem2  38496  mbfposadd  38505  itg2addnclem  38509  itg2gt0cn  38513  ibladdnclem  38514  itgaddnclem1  38516  iblabsnclem  38521  iblabsnc  38522  iblmulc2nc  38523  itggt0cn  38528  ftc1anclem4  38534  ftc1anclem5  38535  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  areacirclem5  38550  areacirc  38551  fdc  38599  heiborlem4  38668  ac6s6  39024  cdleme27a  41344  cdleme31sn1  41358  cdleme31fv1  41368  cdlemk40t  41895  dihvalb  42214  sticksstones12a  43127  brif2  43198  brif12  43199  evlsbagval  43536  fsuppind  43540  dffltz  43584  pw2f1ocnv  43982  aomclem5  44003  kelac1  44008  arearect  44160  areaquad  44161  oe0rif  44230  cantnfresb  44269  safesnsupfidom1o  44361  safesnsupfilb  44362  clsk1indlem1  44989  refsum2cnlem1  45975  upbdrech2  46245  lptioo2  46565  lptioo1  46566  limsupmnfuzlem  46658  limsupre3uzlem  46667  limsup10exlem  46704  coskpi2  46798  cosknegpi  46801  cncfiooicclem1  46825  cncfiooiccre  46827  dvnxpaek  46874  dvnprodlem1  46878  dvnprodlem3  46880  itgioocnicc  46909  iblcncfioo  46910  volico  46915  sublevolico  46916  volioore  46922  voliooico  46924  voliccico  46931  dirkerper  47028  dirkertrigeq  47033  dirkercncflem2  47036  fourierdlem10  47049  fourierdlem32  47071  fourierdlem33  47072  fourierdlem37  47076  fourierdlem62  47100  fourierdlem73  47111  fourierdlem74  47112  fourierdlem75  47113  fourierdlem79  47117  fourierdlem81  47119  fourierdlem82  47120  fourierdlem93  47131  fourierdlem97  47135  fourierdlem101  47139  fourierdlem103  47141  fourierdlem104  47142  sqwvfoura  47160  sqwvfourb  47161  fourierswlem  47162  fouriersw  47163  etransclem4  47170  etransclem15  47181  etransclem19  47185  etransclem20  47186  etransclem23  47189  etransclem24  47190  etransclem25  47191  etransclem27  47193  etransclem31  47197  etransclem32  47198  ioorrnopnxrlem  47238  nnfoctbdjlem  47387  isomenndlem  47462  ovn0val  47482  hoidmv0val  47515  hsphoidmvle2  47517  hoidmv1lelem1  47523  hoidmv1lelem2  47524  hoidmv1le  47526  hoidmvlelem2  47528  hoidmvlelem3  47529  ovnhoilem1  47533  hspdifhsp  47548  hoidifhspdmvle  47552  hspmbllem1  47558  hspmbllem2  47559  hspmbl  47561  volico2  47573  ovnsubadd2lem  47577  ovolval4lem2  47582  ovolval5lem1  47584  afvfundmfveq  48130  dfatafv2iota  48202  dfatafv2eqfv  48253  difmodm1lt  48357  prproropf1olem3  48509  prproropf1olem4  48510  linc1  49459  lincext3  49490  lindslinindsimp1  49491  el0ldep  49500  islindeps2  49517  itcoval0  49696  ackval0  49714  crosspv1d  50882  crosspv2d  50883  veronesev1lem  50895  veronesev2lem  50896  veronesev3lem  50897  veronesev4lem  50898  veronesev5lem  50899  veronesev6lem  50900  veronesevrowd  50901