Theorem iftrue 4492

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142  {cab 2740  ifcif 4486

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487

This theorem is used by:  iftruei  4493  iftrued  4494  iftrueb  4499  ifsb  4500  ifbi  4509  ifeq2da  4519  ifeq12da  4520  ifclda  4522  ifeqda  4523  elimif  4524  ifbothda  4525  ifid  4527  ifeqor  4538  ifnot  4539  ifan  4540  ifor  4541  2if2  4542  dedth  4545  elimhyp  4552  elimhyp2v  4553  elimhyp3v  4554  elimhyp4v  4555  elimdhyp  4557  keephyp2v  4559  keephyp3v  4560  dfopif  4834  dfopg  4835  somin1  6132  somincom  6133  xpima1  6180  elimdelov  7508  brif1  7509  ovif12  7512  ifmpt2v  7514  tz7.44-1  8391  rdg0n  8419  resixpfo  8932  boxriin  8936  boxcutc  8937  pw2f1olem  9067  unxpdomlem2  9215  unxpdomlem3  9216  infsupprpr  9464  ordtypelem1  9478  wemaplem2  9507  unwdomg  9544  ixpiunwdom  9550  cantnfp1lem2  9646  cantnfp1lem3  9647  ssttrcl  9682  ttrclselem2  9693  acndom  10042  dfac12lem2  10135  fin23lem14  10323  axcc2lem  10426  pwfseqlem2  10650  indval2  12229  ind1  12233  uzin  12904  xrmax1  13207  xrmax2  13208  xrmin1  13209  xrmin2  13210  max1ALT  13218  max0sub  13228  ifle  13229  xmulneg1  13301  fzprval  13620  fztpval  13621  modifeq2int  13976  seqf1olem1  14084  seqf1olem2  14085  bcval2  14348  tpf1ofv0  14540  tpf1ofv1  14541  ccatval1  14621  ccatalpha  14638  swrdccat  14779  pfxccat3a  14782  swrdccat3b  14784  repswswrd  14828  cshword  14835  0csh0  14837  ccatco  14879  sgnn  15138  max0add  15368  absmax  15388  sumrblem  15769  fsumcvg  15770  summolem2a  15773  isum  15777  sumss  15782  sumss2  15784  fsumcvg2  15785  fsumser  15788  fsumsplit  15799  sumsplit  15826  prodrblem  15990  fprodcvg  15991  prodmolem2a  15995  zprod  15998  iprod  15999  iprodn0  16001  prodss  16008  fprodsplit  16027  ruclem2  16294  ruclem3  16295  flodddiv4  16479  sadadd2lem2  16514  sadcf  16517  sadc0  16518  sadcp1  16519  sadcaddlem  16521  smupf  16542  smup0  16543  gcd0val  16561  dfgcd2  16610  eucalgf  16647  eucalginv  16648  eucalglt  16649  lcmf0val  16686  phisum  16856  pc0  16920  pcgcd  16944  pcmptcl  16957  pcmpt  16958  pcmpt2  16959  pcprod  16961  fldivp1  16963  prmreclem2  16983  prmreclem4  16985  1arithlem4  16992  vdwlem6  17052  ramtcl2  17077  ramcl2  17082  ramub1lem1  17092  prmop1  17104  fvprmselelfz  17110  fvprmselgcd1  17111  ressid2  17300  xpsfrnel  17622  xpsaddlem  17633  xpsvsca  17637  mreexexd  17710  gsumval1  18747  mgm2nsgrplem2  18987  sgrp2nmndlem2  18992  symgextfve  19495  symgfixfolem1  19514  pmtrmvd  19532  pmtrfinv  19537  pmtrprfval  19563  pmtrprfvalrn  19564  frgpuptinv  19847  frgpup2  19852  frgpup3lem  19853  cyggex  19974  gsumzsplit  20003  gsummpt1n0  20041  dprdfid  20095  dmdprdsplitlem  20115  sdrgacs  20915  abvtrivd  20946  znf1o  21712  uvcvv1  21950  psrlidm  22122  psrridm  22123  mvrf1  22146  mplmonmul  22198  mplcoe1  22199  mplcoe3  22200  mplcoe5  22202  mplmon2  22223  subrgasclcl  22229  evlslem3  22242  evlslem1  22244  selvvvval  22304  psdmul  22340  psdmvr  22343  coe1tmfv1  22446  ply1sclid  22460  dmatmul  22665  scmatscmiddistr  22676  1mavmul  22716  mulmarep1gsum2  22742  1marepvmarrepid  22743  mdetdiag  22767  mdetralt2  22777  mdetunilem2  22781  mdetunilem7  22786  mdetunilem8  22787  mdetunilem9  22788  mndifsplit  22804  maducoeval2  22808  madugsum  22811  madurid  22812  gsummatr01lem3  22825  gsummatr01  22827  smadiadetglem2  22840  1elcpmat  22883  decpmatid  22938  chfacfscmulgsum  23028  chfacfpmmulgsum  23032  ptpjpre1  23739  ptbasfi  23749  ptpjopn  23780  isfcls  24177  ptcmplem2  24221  ptcmplem3  24222  tsmssplit  24320  dscmet  24740  dscopn  24741  icccmplem2  24992  iccpnfcnv  25114  xrhmeo  25116  pcopt  25192  pcopt2  25193  pcoass  25194  pcorevlem  25196  cmetcaulem  25458  ovolicc1  25686  ioorcl  25747  i1f1lem  25859  itg11  25861  itg1addlem2  25867  itg1addlem4  25869  i1fres  25875  itg1climres  25884  mbfi1fseqlem4  25888  mbfi1fseqlem5  25889  mbfi1flim  25893  itg2const2  25911  itg2seq  25912  itg2uba  25913  itg2splitlem  25918  itg2split  25919  itg2monolem1  25920  itg2cnlem1  25931  itg2cnlem2  25932  iblcnlem  25959  iblss  25975  iblss2  25976  itgitg2  25977  itgle  25980  itgss  25982  itgss2  25983  itgss3  25985  itgless  25987  ibladdlem  25990  itgaddlem1  25993  iblabslem  25998  iblabs  25999  iblabsr  26000  iblmulc2  26001  bddmulibl  26009  bddiblnc  26012  itggt0  26014  itgcn  26015  limcvallem  26041  ellimc2  26047  limccnp  26061  limccnp2  26062  limcco  26063  dvcobr  26116  dvexp2  26124  mon1pid  26322  elply2  26364  elplyd  26370  ply1termlem  26371  coe1termlem  26426  abelthlem9  26614  logtayl  26836  leibpilem2  27117  leibpi  27118  rlimcnp2  27142  efrlim  27145  igamz  27223  isnsqf  27310  mule1  27323  sqff1o  27357  muinv  27368  chtublem  27386  dchrelbasd  27414  bposlem1  27459  bposlem3  27461  bposlem5  27463  bposlem6  27464  lgsval2lem  27482  lgsneg  27496  lgsdilem  27499  lgsdir2  27505  lgsdir  27507  lgsdi  27509  lgsne0  27510  gausslemma2dlem1a  27540  2lgslem1c  27568  2lgslem3  27579  2lgs  27582  dchrvmasum2if  27672  dchrvmasumiflem1  27676  rpvmasum2  27687  pntrlog2bndlem4  27755  pntrlog2bndlem5  27756  padicabv  27805  ostth2lem4  27811  nosupno  27878  nosupbday  27880  nosupbnd1  27889  nosupbnd2  27891  noinfno  27893  noinfbday  27895  noinfbnd1  27904  maxs1  27944  maxs2  27945  mins1  27946  mins2  27947  abssid  28445  abssge0  28449  axlowdimlem15  29317  opvtxval  29364  opiedgval  29367  elimifd  32900  elim2if  32901  ifeq3da  32903  ifnefals  32905  fmptunsnop  33056  pmtridf1o  33423  fzto1stfv1  33430  resvid2  33659  psrmonmul  33949  vieta  33979  2sqr3minply  34179  cos9thpiminply  34187  xrge0iifcnv  34332  xrge0iifiso  34334  xrge0iifhom  34336  sigaclfu2  34520  ddeval1  34633  eulerpartlemb  34767  ballotlemsima  34915  ballotlemrv1  34920  signsw0glem  34949  signswmnd  34953  signswrid  34954  vonf1oonfo  35607  indispconn  35734  ex-sategoelel  35921  ex-sategoelelomsuc  35926  ex-sategoelel12  35927  mrsubvr  36011  dfrdg2  36293  dfrdg3  36294  unisnif  36423  dfrdg4  36451  fnejoin2  36908  unbdqndv2lem2  37127  bj-xpima2sn  37622  finxpreclem1  38063  finxpreclem3  38067  matunitlindflem1  38295  poimirlem2  38301  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem24  38323  mblfinlem2  38337  mbfposadd  38346  itg2addnclem  38350  itg2gt0cn  38354  ibladdnclem  38355  itgaddnclem1  38357  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  itggt0cn  38369  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  areacirclem5  38391  areacirc  38392  fdc  38424  heiborlem4  38493  ac6s6  38849  cdleme27a  41169  cdleme31sn1  41183  cdleme31fv1  41193  cdlemk40t  41720  dihvalb  42039  sticksstones12a  42952  brif2  43023  brif12  43024  evlsbagval  43346  fsuppind  43350  dffltz  43394  pw2f1ocnv  43792  aomclem5  43813  kelac1  43818  arearect  43970  areaquad  43971  oe0rif  44040  cantnfresb  44079  safesnsupfidom1o  44171  safesnsupfilb  44172  clsk1indlem1  44799  refsum2cnlem1  45785  upbdrech2  46055  lptioo2  46375  lptioo1  46376  limsupmnfuzlem  46468  limsupre3uzlem  46477  limsup10exlem  46514  coskpi2  46608  cosknegpi  46611  cncfiooicclem1  46635  cncfiooiccre  46637  dvnxpaek  46684  dvnprodlem1  46688  dvnprodlem3  46690  itgioocnicc  46719  iblcncfioo  46720  volico  46725  sublevolico  46726  volioore  46732  voliooico  46734  voliccico  46741  dirkerper  46838  dirkertrigeq  46843  dirkercncflem2  46846  fourierdlem10  46859  fourierdlem32  46881  fourierdlem33  46882  fourierdlem37  46886  fourierdlem62  46910  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem79  46927  fourierdlem81  46929  fourierdlem82  46930  fourierdlem93  46941  fourierdlem97  46945  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  etransclem4  46980  etransclem15  46991  etransclem19  46995  etransclem20  46996  etransclem23  46999  etransclem24  47000  etransclem25  47001  etransclem27  47003  etransclem31  47007  etransclem32  47008  ioorrnopnxrlem  47048  nnfoctbdjlem  47197  isomenndlem  47272  ovn0val  47292  hoidmv0val  47325  hsphoidmvle2  47327  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmv1le  47336  hoidmvlelem2  47338  hoidmvlelem3  47339  ovnhoilem1  47343  hspdifhsp  47358  hoidifhspdmvle  47362  hspmbllem1  47368  hspmbllem2  47369  hspmbl  47371  volico2  47383  ovnsubadd2lem  47387  ovolval4lem2  47392  ovolval5lem1  47394  afvfundmfveq  47903  dfatafv2iota  47975  dfatafv2eqfv  48026  difmodm1lt  48130  prproropf1olem3  48282  prproropf1olem4  48283  linc1  49233  lincext3  49264  lindslinindsimp1  49265  el0ldep  49274  islindeps2  49291  itcoval0  49470  ackval0  49488  crosspv1i  50669  crosspv2i  50670