Theorem iftrue 4484

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  iftruei  4485  iftrued  4486  iftrueb  4491  ifsb  4492  ifbi  4501  ifeq2da  4511  ifeq12da  4512  ifclda  4514  ifeqda  4515  elimif  4516  ifbothda  4517  ifid  4519  ifeqor  4530  ifnot  4531  ifan  4532  ifor  4533  2if2  4534  dedth  4537  elimhyp  4544  elimhyp2v  4545  elimhyp3v  4546  elimhyp4v  4547  elimdhyp  4549  keephyp2v  4551  keephyp3v  4552  dfopif  4824  dfopg  4825  somin1  6086  somincom  6087  xpima1  6136  elimdelov  7449  brif1  7450  ovif12  7453  ifmpt2v  7455  tz7.44-1  8335  rdg0n  8363  resixpfo  8870  boxriin  8874  boxcutc  8875  pw2f1olem  9005  unxpdomlem2  9156  unxpdomlem3  9157  infsupprpr  9415  ordtypelem1  9429  wemaplem2  9458  unwdomg  9495  ixpiunwdom  9501  cantnfp1lem2  9594  cantnfp1lem3  9595  ssttrcl  9630  ttrclselem2  9641  acndom  9964  dfac12lem2  10058  fin23lem14  10246  axcc2lem  10349  pwfseqlem2  10572  uzin  12793  xrmax1  13095  xrmax2  13096  xrmin1  13097  xrmin2  13098  max1ALT  13106  max0sub  13116  ifle  13117  xmulneg1  13189  fzprval  13506  fztpval  13507  modifeq2int  13858  seqf1olem1  13966  seqf1olem2  13967  bcval2  14230  tpf1ofv0  14421  tpf1ofv1  14422  ccatval1  14502  ccatalpha  14518  swrdccat  14659  pfxccat3a  14662  swrdccat3b  14664  repswswrd  14708  cshword  14715  0csh0  14717  ccatco  14760  sgnn  15019  max0add  15235  absmax  15255  sumrblem  15636  fsumcvg  15637  summolem2a  15640  isum  15644  sumss  15649  sumss2  15651  fsumcvg2  15652  fsumser  15655  fsumsplit  15666  sumsplit  15693  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  zprod  15862  iprod  15863  iprodn0  15865  prodss  15872  fprodsplit  15891  ruclem2  16159  ruclem3  16160  flodddiv4  16344  sadadd2lem2  16379  sadcf  16382  sadc0  16383  sadcp1  16384  sadcaddlem  16386  smupf  16407  smup0  16408  gcd0val  16426  dfgcd2  16475  eucalgf  16512  eucalginv  16513  eucalglt  16514  lcmf0val  16551  phisum  16720  pc0  16784  pcgcd  16808  pcmptcl  16821  pcmpt  16822  pcmpt2  16823  pcprod  16825  fldivp1  16827  prmreclem2  16847  prmreclem4  16849  1arithlem4  16856  vdwlem6  16916  ramtcl2  16941  ramcl2  16946  ramub1lem1  16956  prmop1  16968  fvprmselelfz  16974  fvprmselgcd1  16975  ressid2  17163  xpsfrnel  17484  xpsaddlem  17495  xpsvsca  17499  mreexexd  17572  gsumval1  18575  mgm2nsgrplem2  18811  sgrp2nmndlem2  18816  symgextfve  19316  symgfixfolem1  19335  pmtrmvd  19353  pmtrfinv  19358  pmtrprfval  19384  pmtrprfvalrn  19385  frgpuptinv  19668  frgpup2  19673  frgpup3lem  19674  cyggex  19795  gsumzsplit  19824  gsummpt1n0  19862  dprdfid  19916  dmdprdsplitlem  19936  sdrgacs  20704  abvtrivd  20735  znf1o  21476  uvcvv1  21714  psrlidm  21887  psrridm  21888  mvrf1  21911  mplmonmul  21959  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  mplmon2  21984  subrgasclcl  21990  evlslem3  22003  evlslem1  22005  psdmul  22069  psdmvr  22072  coe1tmfv1  22176  ply1sclid  22190  dmatmul  22400  scmatscmiddistr  22411  1mavmul  22451  mulmarep1gsum2  22477  1marepvmarrepid  22478  mdetdiag  22502  mdetralt2  22512  mdetunilem2  22516  mdetunilem7  22521  mdetunilem8  22522  mdetunilem9  22523  mndifsplit  22539  maducoeval2  22543  madugsum  22546  madurid  22547  gsummatr01lem3  22560  gsummatr01  22562  smadiadetglem2  22575  1elcpmat  22618  decpmatid  22673  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  ptpjpre1  23474  ptbasfi  23484  ptpjopn  23515  isfcls  23912  ptcmplem2  23956  ptcmplem3  23957  tsmssplit  24055  dscmet  24476  dscopn  24477  icccmplem2  24728  iccpnfcnv  24858  xrhmeo  24860  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  cmetcaulem  25204  ovolicc1  25433  ioorcl  25494  i1f1lem  25606  itg11  25608  itg1addlem2  25614  itg1addlem4  25616  i1fres  25622  itg1climres  25631  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1flim  25640  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2cnlem1  25678  itg2cnlem2  25679  iblcnlem  25706  iblss  25722  iblss2  25723  itgitg2  25724  itgle  25727  itgss  25729  itgss2  25730  itgss3  25732  itgless  25734  ibladdlem  25737  itgaddlem1  25740  iblabslem  25745  iblabs  25746  iblabsr  25747  iblmulc2  25748  bddmulibl  25756  bddiblnc  25759  itggt0  25761  itgcn  25762  limcvallem  25788  ellimc2  25794  limccnp  25808  limccnp2  25809  limcco  25810  dvcobr  25865  dvcobrOLD  25866  dvexp2  25874  mon1pid  26075  elply2  26117  elplyd  26123  ply1termlem  26124  coe1termlem  26179  abelthlem9  26366  logtayl  26585  leibpilem2  26867  leibpi  26868  rlimcnp2  26892  efrlim  26895  efrlimOLD  26896  igamz  26974  isnsqf  27061  mule1  27074  sqff1o  27108  muinv  27119  chtublem  27138  dchrelbasd  27166  bposlem1  27211  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgsval2lem  27234  lgsneg  27248  lgsdilem  27251  lgsdir2  27257  lgsdir  27259  lgsdi  27261  lgsne0  27262  gausslemma2dlem1a  27292  2lgslem1c  27320  2lgslem3  27331  2lgs  27334  dchrvmasum2if  27424  dchrvmasumiflem1  27428  rpvmasum2  27439  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  padicabv  27557  ostth2lem4  27563  nosupno  27631  nosupbday  27633  nosupbnd1  27642  nosupbnd2  27644  noinfno  27646  noinfbday  27648  noinfbnd1  27657  maxs1  27693  maxs2  27694  mins1  27695  mins2  27696  abssid  28166  abssge0  28170  axlowdimlem15  28919  opvtxval  28966  opiedgval  28969  elimifd  32505  elim2if  32506  ifeq3da  32508  ifnefals  32510  fmptunsnop  32656  indval2  32810  ind1  32813  pmtridf1o  33049  fzto1stfv1  33056  resvid2  33278  2sqr3minply  33746  cos9thpiminply  33754  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  sigaclfu2  34087  ddeval1  34200  eulerpartlemb  34335  ballotlemsima  34483  ballotlemrv1  34488  signsw0glem  34520  signswmnd  34524  signswrid  34525  indispconn  35206  ex-sategoelel  35393  ex-sategoelelomsuc  35398  ex-sategoelel12  35399  mrsubvr  35483  dfrdg2  35768  dfrdg3  35769  unisnif  35898  dfrdg4  35924  fnejoin2  36342  unbdqndv2lem2  36483  bj-xpima2sn  36931  finxpreclem1  37362  finxpreclem3  37366  matunitlindflem1  37595  poimirlem2  37601  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem24  37623  mblfinlem2  37637  mbfposadd  37646  itg2addnclem  37650  itg2gt0cn  37654  ibladdnclem  37655  itgaddnclem1  37657  iblabsnclem  37662  iblabsnc  37663  iblmulc2nc  37664  itggt0cn  37669  ftc1anclem4  37675  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  areacirclem5  37691  areacirc  37692  fdc  37724  heiborlem4  37793  ac6s6  38151  cdleme27a  40346  cdleme31sn1  40360  cdleme31fv1  40370  cdlemk40t  40897  dihvalb  41216  sticksstones12a  42130  brif2  42197  brif12  42198  evlsbagval  42539  selvvvval  42558  fsuppind  42563  dffltz  42607  pw2f1ocnv  43010  aomclem5  43031  kelac1  43036  arearect  43188  areaquad  43189  oe0rif  43258  cantnfresb  43297  safesnsupfidom1o  43390  safesnsupfilb  43391  clsk1indlem1  44018  refsum2cnlem1  45015  upbdrech2  45290  lptioo2  45613  lptioo1  45614  limsupmnfuzlem  45708  limsupre3uzlem  45717  limsup10exlem  45754  coskpi2  45848  cosknegpi  45851  cncfiooicclem1  45875  cncfiooiccre  45877  dvnxpaek  45924  dvnprodlem1  45928  dvnprodlem3  45930  itgioocnicc  45959  iblcncfioo  45960  volico  45965  sublevolico  45966  volioore  45972  voliooico  45974  voliccico  45981  dirkerper  46078  dirkertrigeq  46083  dirkercncflem2  46086  fourierdlem10  46099  fourierdlem32  46121  fourierdlem33  46122  fourierdlem37  46126  fourierdlem62  46150  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem79  46167  fourierdlem81  46169  fourierdlem82  46170  fourierdlem93  46181  fourierdlem97  46185  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  etransclem4  46220  etransclem15  46231  etransclem19  46235  etransclem20  46236  etransclem23  46239  etransclem24  46240  etransclem25  46241  etransclem27  46243  etransclem31  46247  etransclem32  46248  ioorrnopnxrlem  46288  nnfoctbdjlem  46437  isomenndlem  46512  ovn0val  46532  hoidmv0val  46565  hsphoidmvle2  46567  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmv1le  46576  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoilem1  46583  hspdifhsp  46598  hoidifhspdmvle  46602  hspmbllem1  46608  hspmbllem2  46609  hspmbl  46611  volico2  46623  ovnsubadd2lem  46627  ovolval4lem2  46632  ovolval5lem1  46634  afvfundmfveq  47123  dfatafv2iota  47195  dfatafv2eqfv  47246  difmodm1lt  47344  prproropf1olem3  47490  prproropf1olem4  47491  linc1  48398  lincext3  48429  lindslinindsimp1  48430  el0ldep  48439  islindeps2  48456  itcoval0  48635  ackval0  48653