Theorem iftrue 4486

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  iftruei  4487  iftrued  4488  iftrueb  4493  ifsb  4494  ifbi  4503  ifeq2da  4513  ifeq12da  4514  ifclda  4516  ifeqda  4517  elimif  4518  ifbothda  4519  ifid  4521  ifeqor  4532  ifnot  4533  ifan  4534  ifor  4535  2if2  4536  dedth  4539  elimhyp  4546  elimhyp2v  4547  elimhyp3v  4548  elimhyp4v  4549  elimdhyp  4551  keephyp2v  4553  keephyp3v  4554  dfopif  4827  dfopg  4828  somin1  6091  somincom  6092  xpima1  6142  elimdelov  7456  brif1  7457  ovif12  7460  ifmpt2v  7462  tz7.44-1  8339  rdg0n  8367  resixpfo  8878  boxriin  8882  boxcutc  8883  pw2f1olem  9013  unxpdomlem2  9161  unxpdomlem3  9162  infsupprpr  9413  ordtypelem1  9427  wemaplem2  9456  unwdomg  9493  ixpiunwdom  9499  cantnfp1lem2  9592  cantnfp1lem3  9593  ssttrcl  9628  ttrclselem2  9639  acndom  9965  dfac12lem2  10059  fin23lem14  10247  axcc2lem  10350  pwfseqlem2  10574  uzin  12791  xrmax1  13094  xrmax2  13095  xrmin1  13096  xrmin2  13097  max1ALT  13105  max0sub  13115  ifle  13116  xmulneg1  13188  fzprval  13505  fztpval  13506  modifeq2int  13860  seqf1olem1  13968  seqf1olem2  13969  bcval2  14232  tpf1ofv0  14423  tpf1ofv1  14424  ccatval1  14504  ccatalpha  14521  swrdccat  14662  pfxccat3a  14665  swrdccat3b  14667  repswswrd  14711  cshword  14718  0csh0  14720  ccatco  14762  sgnn  15021  max0add  15237  absmax  15257  sumrblem  15638  fsumcvg  15639  summolem2a  15642  isum  15646  sumss  15651  sumss2  15653  fsumcvg2  15654  fsumser  15657  fsumsplit  15668  sumsplit  15695  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  zprod  15864  iprod  15865  iprodn0  15867  prodss  15874  fprodsplit  15893  ruclem2  16161  ruclem3  16162  flodddiv4  16346  sadadd2lem2  16381  sadcf  16384  sadc0  16385  sadcp1  16386  sadcaddlem  16388  smupf  16409  smup0  16410  gcd0val  16428  dfgcd2  16477  eucalgf  16514  eucalginv  16515  eucalglt  16516  lcmf0val  16553  phisum  16722  pc0  16786  pcgcd  16810  pcmptcl  16823  pcmpt  16824  pcmpt2  16825  pcprod  16827  fldivp1  16829  prmreclem2  16849  prmreclem4  16851  1arithlem4  16858  vdwlem6  16918  ramtcl2  16943  ramcl2  16948  ramub1lem1  16958  prmop1  16970  fvprmselelfz  16976  fvprmselgcd1  16977  ressid2  17165  xpsfrnel  17487  xpsaddlem  17498  xpsvsca  17502  mreexexd  17575  gsumval1  18612  mgm2nsgrplem2  18848  sgrp2nmndlem2  18853  symgextfve  19352  symgfixfolem1  19371  pmtrmvd  19389  pmtrfinv  19394  pmtrprfval  19420  pmtrprfvalrn  19421  frgpuptinv  19704  frgpup2  19709  frgpup3lem  19710  cyggex  19831  gsumzsplit  19860  gsummpt1n0  19898  dprdfid  19952  dmdprdsplitlem  19972  sdrgacs  20738  abvtrivd  20769  znf1o  21510  uvcvv1  21748  psrlidm  21921  psrridm  21922  mvrf1  21945  mplmonmul  21995  mplcoe1  21996  mplcoe3  21997  mplcoe5  21999  mplmon2  22020  subrgasclcl  22026  evlslem3  22039  evlslem1  22041  psdmul  22113  psdmvr  22116  coe1tmfv1  22220  ply1sclid  22234  dmatmul  22445  scmatscmiddistr  22456  1mavmul  22496  mulmarep1gsum2  22522  1marepvmarrepid  22523  mdetdiag  22547  mdetralt2  22557  mdetunilem2  22561  mdetunilem7  22566  mdetunilem8  22567  mdetunilem9  22568  mndifsplit  22584  maducoeval2  22588  madugsum  22591  madurid  22592  gsummatr01lem3  22605  gsummatr01  22607  smadiadetglem2  22620  1elcpmat  22663  decpmatid  22718  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  ptpjpre1  23519  ptbasfi  23529  ptpjopn  23560  isfcls  23957  ptcmplem2  24001  ptcmplem3  24002  tsmssplit  24100  dscmet  24520  dscopn  24521  icccmplem2  24772  iccpnfcnv  24902  xrhmeo  24904  pcopt  24982  pcopt2  24983  pcoass  24984  pcorevlem  24986  cmetcaulem  25248  ovolicc1  25477  ioorcl  25538  i1f1lem  25650  itg11  25652  itg1addlem2  25658  itg1addlem4  25660  i1fres  25666  itg1climres  25675  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfi1flim  25684  itg2const2  25702  itg2seq  25703  itg2uba  25704  itg2splitlem  25709  itg2split  25710  itg2monolem1  25711  itg2cnlem1  25722  itg2cnlem2  25723  iblcnlem  25750  iblss  25766  iblss2  25767  itgitg2  25768  itgle  25771  itgss  25773  itgss2  25774  itgss3  25776  itgless  25778  ibladdlem  25781  itgaddlem1  25784  iblabslem  25789  iblabs  25790  iblabsr  25791  iblmulc2  25792  bddmulibl  25800  bddiblnc  25803  itggt0  25805  itgcn  25806  limcvallem  25832  ellimc2  25838  limccnp  25852  limccnp2  25853  limcco  25854  dvcobr  25909  dvcobrOLD  25910  dvexp2  25918  mon1pid  26119  elply2  26161  elplyd  26167  ply1termlem  26168  coe1termlem  26223  abelthlem9  26410  logtayl  26629  leibpilem2  26911  leibpi  26912  rlimcnp2  26936  efrlim  26939  efrlimOLD  26940  igamz  27018  isnsqf  27105  mule1  27118  sqff1o  27152  muinv  27163  chtublem  27182  dchrelbasd  27210  bposlem1  27255  bposlem3  27257  bposlem5  27259  bposlem6  27260  lgsval2lem  27278  lgsneg  27292  lgsdilem  27295  lgsdir2  27301  lgsdir  27303  lgsdi  27305  lgsne0  27306  gausslemma2dlem1a  27336  2lgslem1c  27364  2lgslem3  27375  2lgs  27378  dchrvmasum2if  27468  dchrvmasumiflem1  27472  rpvmasum2  27483  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  padicabv  27601  ostth2lem4  27607  nosupno  27675  nosupbday  27677  nosupbnd1  27686  nosupbnd2  27688  noinfno  27690  noinfbday  27692  noinfbnd1  27701  maxs1  27741  maxs2  27742  mins1  27743  mins2  27744  abssid  28222  abssge0  28226  axlowdimlem15  29012  opvtxval  29059  opiedgval  29062  elimifd  32600  elim2if  32601  ifeq3da  32603  ifnefals  32605  fmptunsnop  32760  indval2  32914  ind1  32917  pmtridf1o  33157  fzto1stfv1  33164  resvid2  33392  vieta  33717  2sqr3minply  33918  cos9thpiminply  33926  xrge0iifcnv  34071  xrge0iifiso  34073  xrge0iifhom  34075  sigaclfu2  34259  ddeval1  34372  eulerpartlemb  34506  ballotlemsima  34654  ballotlemrv1  34659  signsw0glem  34691  signswmnd  34695  signswrid  34696  indispconn  35409  ex-sategoelel  35596  ex-sategoelelomsuc  35601  ex-sategoelel12  35602  mrsubvr  35686  dfrdg2  35968  dfrdg3  35969  unisnif  36098  dfrdg4  36126  fnejoin2  36544  unbdqndv2lem2  36685  bj-xpima2sn  37134  finxpreclem1  37565  finxpreclem3  37569  matunitlindflem1  37788  poimirlem2  37794  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem19  37811  poimirlem20  37812  poimirlem24  37816  mblfinlem2  37830  mbfposadd  37839  itg2addnclem  37843  itg2gt0cn  37847  ibladdnclem  37848  itgaddnclem1  37850  iblabsnclem  37855  iblabsnc  37856  iblmulc2nc  37857  itggt0cn  37862  ftc1anclem4  37868  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  areacirclem5  37884  areacirc  37885  fdc  37917  heiborlem4  37986  ac6s6  38344  cdleme27a  40664  cdleme31sn1  40678  cdleme31fv1  40688  cdlemk40t  41215  dihvalb  41534  sticksstones12a  42448  brif2  42517  brif12  42518  evlsbagval  42848  selvvvval  42864  fsuppind  42869  dffltz  42913  pw2f1ocnv  43315  aomclem5  43336  kelac1  43341  arearect  43493  areaquad  43494  oe0rif  43563  cantnfresb  43602  safesnsupfidom1o  43694  safesnsupfilb  43695  clsk1indlem1  44322  refsum2cnlem1  45318  upbdrech2  45592  lptioo2  45913  lptioo1  45914  limsupmnfuzlem  46006  limsupre3uzlem  46015  limsup10exlem  46052  coskpi2  46146  cosknegpi  46149  cncfiooicclem1  46173  cncfiooiccre  46175  dvnxpaek  46222  dvnprodlem1  46226  dvnprodlem3  46228  itgioocnicc  46257  iblcncfioo  46258  volico  46263  sublevolico  46264  volioore  46270  voliooico  46272  voliccico  46279  dirkerper  46376  dirkertrigeq  46381  dirkercncflem2  46384  fourierdlem10  46397  fourierdlem32  46419  fourierdlem33  46420  fourierdlem37  46424  fourierdlem62  46448  fourierdlem73  46459  fourierdlem74  46460  fourierdlem75  46461  fourierdlem79  46465  fourierdlem81  46467  fourierdlem82  46468  fourierdlem93  46479  fourierdlem97  46483  fourierdlem101  46487  fourierdlem103  46489  fourierdlem104  46490  sqwvfoura  46508  sqwvfourb  46509  fourierswlem  46510  fouriersw  46511  etransclem4  46518  etransclem15  46529  etransclem19  46533  etransclem20  46534  etransclem23  46537  etransclem24  46538  etransclem25  46539  etransclem27  46541  etransclem31  46545  etransclem32  46546  ioorrnopnxrlem  46586  nnfoctbdjlem  46735  isomenndlem  46810  ovn0val  46830  hoidmv0val  46863  hsphoidmvle2  46865  hoidmv1lelem1  46871  hoidmv1lelem2  46872  hoidmv1le  46874  hoidmvlelem2  46876  hoidmvlelem3  46877  ovnhoilem1  46881  hspdifhsp  46896  hoidifhspdmvle  46900  hspmbllem1  46906  hspmbllem2  46907  hspmbl  46909  volico2  46921  ovnsubadd2lem  46925  ovolval4lem2  46930  ovolval5lem1  46932  afvfundmfveq  47420  dfatafv2iota  47492  dfatafv2eqfv  47543  difmodm1lt  47641  prproropf1olem3  47787  prproropf1olem4  47788  linc1  48707  lincext3  48738  lindslinindsimp1  48739  el0ldep  48748  islindeps2  48765  itcoval0  48944  ackval0  48962