Theorem iftrue 4462

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 4458	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1040	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	abbi2dv 2876	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2798	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  iftruei  4463  iftrued  4464  ifsb  4469  ifbi  4478  ifeq2da  4488  ifeq12da  4489  ifclda  4491  ifeqda  4492  elimif  4493  ifbothda  4494  ifid  4496  ifeqor  4507  ifnot  4508  ifan  4509  ifor  4510  2if2  4511  dedth  4514  elimhyp  4521  elimhyp2v  4522  elimhyp3v  4523  elimhyp4v  4524  elimdhyp  4526  keephyp2v  4528  keephyp3v  4529  dfopifOLD  4798  dfopg  4799  somin1  6027  somincom  6028  xpima1  6075  elimdelov  7349  ovif12  7352  tz7.44-1  8208  resixpfo  8682  boxriin  8686  boxcutc  8687  pw2f1olem  8816  unxpdomlem2  8957  unxpdomlem3  8958  infsupprpr  9193  ordtypelem1  9207  wemaplem2  9236  unwdomg  9273  ixpiunwdom  9279  cantnfp1lem2  9367  cantnfp1lem3  9368  acndom  9738  dfac12lem2  9831  fin23lem14  10020  axcc2lem  10123  pwfseqlem2  10346  uzin  12547  xrmax1  12838  xrmax2  12839  xrmin1  12840  xrmin2  12841  max1ALT  12849  max0sub  12859  ifle  12860  xmulneg1  12932  fzprval  13246  fztpval  13247  modifeq2int  13581  seqf1olem1  13690  seqf1olem2  13691  bcval2  13947  ccatval1  14209  ccatval1OLD  14210  ccatalpha  14226  swrdccat  14376  pfxccat3a  14379  swrdccat3b  14381  repswswrd  14425  cshword  14432  0csh0  14434  ccatco  14476  sgnn  14733  max0add  14950  absmax  14969  sumrblem  15351  fsumcvg  15352  summolem2a  15355  isum  15359  sumss  15364  sumss2  15366  fsumcvg2  15367  fsumser  15370  fsumsplit  15381  sumsplit  15408  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  zprod  15575  iprod  15576  iprodn0  15578  prodss  15585  fprodsplit  15604  ruclem2  15869  ruclem3  15870  flodddiv4  16050  sadadd2lem2  16085  sadcf  16088  sadc0  16089  sadcp1  16090  sadcaddlem  16092  smupf  16113  smup0  16114  gcd0val  16132  dfgcd2  16182  eucalgf  16216  eucalginv  16217  eucalglt  16218  lcmf0val  16255  phisum  16419  pc0  16483  pcgcd  16507  pcmptcl  16520  pcmpt  16521  pcmpt2  16522  pcprod  16524  fldivp1  16526  prmreclem2  16546  prmreclem4  16548  1arithlem4  16555  vdwlem6  16615  ramtcl2  16640  ramcl2  16645  ramub1lem1  16655  prmop1  16667  fvprmselelfz  16673  fvprmselgcd1  16674  ressid2  16871  xpsfrnel  17190  xpsaddlem  17201  xpsvsca  17205  mreexexd  17274  gsumval1  18282  mgm2nsgrplem2  18473  sgrp2nmndlem2  18478  symgextfve  18942  symgfixfolem1  18961  pmtrmvd  18979  pmtrfinv  18984  pmtrprfval  19010  pmtrprfvalrn  19011  frgpuptinv  19292  frgpup2  19297  frgpup3lem  19298  cyggex  19414  gsumzsplit  19443  gsummpt1n0  19481  dprdfid  19535  dmdprdsplitlem  19555  sdrgacs  19984  abvtrivd  20015  znf1o  20671  uvcvv1  20906  psrlidm  21082  psrridm  21083  mvrf1  21104  mplmonmul  21147  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  mplmon2  21179  subrgasclcl  21185  evlslem3  21200  evlslem1  21202  coe1tmfv1  21355  ply1sclid  21369  dmatmul  21554  scmatscmiddistr  21565  1mavmul  21605  mulmarep1gsum2  21631  1marepvmarrepid  21632  mdetdiag  21656  mdetralt2  21666  mdetunilem2  21670  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  mndifsplit  21693  maducoeval2  21697  madugsum  21700  madurid  21701  gsummatr01lem3  21714  gsummatr01  21716  smadiadetglem2  21729  1elcpmat  21772  decpmatid  21827  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  ptpjpre1  22630  ptbasfi  22640  ptpjopn  22671  isfcls  23068  ptcmplem2  23112  ptcmplem3  23113  tsmssplit  23211  dscmet  23634  dscopn  23635  icccmplem2  23892  iccpnfcnv  24013  xrhmeo  24015  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  cmetcaulem  24357  ovolicc1  24585  ioorcl  24646  i1f1lem  24758  itg11  24760  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1flim  24793  itg2const2  24811  itg2seq  24812  itg2uba  24813  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2cnlem1  24831  itg2cnlem2  24832  iblcnlem  24858  iblss  24874  iblss2  24875  itgitg2  24876  itgle  24879  itgss  24881  itgss2  24882  itgss3  24884  itgless  24886  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  bddmulibl  24908  bddiblnc  24911  itggt0  24913  itgcn  24914  limcvallem  24940  ellimc2  24946  limccnp  24960  limccnp2  24961  limcco  24962  dvcobr  25015  dvexp2  25023  elply2  25262  elplyd  25268  ply1termlem  25269  coe1termlem  25324  abelthlem9  25504  logtayl  25720  leibpilem2  25996  leibpi  25997  rlimcnp2  26021  efrlim  26024  igamz  26102  isnsqf  26189  mule1  26202  sqff1o  26236  muinv  26247  chtublem  26264  dchrelbasd  26292  bposlem1  26337  bposlem3  26339  bposlem5  26341  bposlem6  26342  lgsval2lem  26360  lgsneg  26374  lgsdilem  26377  lgsdir2  26383  lgsdir  26385  lgsdi  26387  lgsne0  26388  gausslemma2dlem1a  26418  2lgslem1c  26446  2lgslem3  26457  2lgs  26460  dchrvmasum2if  26550  dchrvmasumiflem1  26554  rpvmasum2  26565  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  padicabv  26683  ostth2lem4  26689  axlowdimlem15  27227  opvtxval  27276  opiedgval  27279  elimifd  30787  elim2if  30788  ifeq3da  30790  pmtridf1o  31263  fzto1stfv1  31270  resvid2  31429  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  indval2  31882  ind1  31885  sigaclfu2  31989  ddeval1  32102  eulerpartlemb  32235  ballotlemsima  32382  ballotlemrv1  32387  signsw0glem  32432  signswmnd  32436  signswrid  32437  indispconn  33096  ex-sategoelel  33283  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  mrsubvr  33373  rdg0n  33598  dfrdg2  33677  dfrdg3  33678  ssttrcl  33701  ttrclselem2  33712  nosupno  33833  nosupbday  33835  nosupbnd1  33844  nosupbnd2  33846  noinfno  33848  noinfbday  33850  noinfbnd1  33859  unisnif  34154  dfrdg4  34180  fnejoin2  34485  unbdqndv2lem2  34617  bj-xpima2sn  35075  finxpreclem1  35487  finxpreclem3  35491  matunitlindflem1  35700  poimirlem2  35706  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  mblfinlem2  35742  mbfposadd  35751  itg2addnclem  35755  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itggt0cn  35774  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirclem5  35796  areacirc  35797  fdc  35830  heiborlem4  35899  ac6s6  36257  cdleme27a  38308  cdleme31sn1  38322  cdleme31fv1  38332  cdlemk40t  38859  dihvalb  39178  sticksstones12a  40041  metakunt5  40057  metakunt6  40058  metakunt10  40062  metakunt11  40063  metakunt20  40072  brif1  40124  brif2  40125  brif12  40126  evlsbagval  40198  fsuppind  40202  dffltz  40387  pw2f1ocnv  40775  aomclem5  40799  kelac1  40804  mon1pid  40946  arearect  40962  areaquad  40963  clsk1indlem1  41544  refsum2cnlem1  42469  upbdrech2  42737  lptioo2  43062  lptioo1  43063  limsupmnfuzlem  43157  limsupre3uzlem  43166  limsup10exlem  43203  coskpi2  43297  cosknegpi  43300  cncfiooicclem1  43324  cncfiooiccre  43326  dvnxpaek  43373  dvnprodlem1  43377  dvnprodlem3  43379  itgioocnicc  43408  iblcncfioo  43409  volico  43414  sublevolico  43415  volioore  43421  voliooico  43423  voliccico  43430  dirkerper  43527  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem10  43548  fourierdlem32  43570  fourierdlem33  43571  fourierdlem37  43575  fourierdlem62  43599  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem93  43630  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem4  43669  etransclem15  43680  etransclem19  43684  etransclem20  43685  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem27  43692  etransclem31  43696  etransclem32  43697  ioorrnopnxrlem  43737  nnfoctbdjlem  43883  isomenndlem  43958  ovn0val  43978  hoidmv0val  44011  hsphoidmvle2  44013  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  hspdifhsp  44044  hoidifhspdmvle  44048  hspmbllem1  44054  hspmbllem2  44055  hspmbl  44057  volico2  44069  ovnsubadd2lem  44073  ovolval4lem2  44078  ovolval5lem1  44080  afvfundmfveq  44517  dfatafv2iota  44589  dfatafv2eqfv  44640  prproropf1olem3  44845  prproropf1olem4  44846  linc1  45654  lincext3  45685  lindslinindsimp1  45686  el0ldep  45695  islindeps2  45712  itcoval0  45896  ackval0  45914