Theorem iftrue 4534

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709  ifcif 4528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  iftruei  4535  iftrued  4536  ifsb  4541  ifbi  4550  ifeq2da  4560  ifeq12da  4561  ifclda  4563  ifeqda  4564  elimif  4565  ifbothda  4566  ifid  4568  ifeqor  4579  ifnot  4580  ifan  4581  ifor  4582  2if2  4583  dedth  4586  elimhyp  4593  elimhyp2v  4594  elimhyp3v  4595  elimhyp4v  4596  elimdhyp  4598  keephyp2v  4600  keephyp3v  4601  dfopif  4870  dfopg  4871  somin1  6134  somincom  6135  xpima1  6182  elimdelov  7507  ovif12  7510  tz7.44-1  8408  rdg0n  8436  resixpfo  8932  boxriin  8936  boxcutc  8937  pw2f1olem  9078  unxpdomlem2  9253  unxpdomlem3  9254  infsupprpr  9501  ordtypelem1  9515  wemaplem2  9544  unwdomg  9581  ixpiunwdom  9587  cantnfp1lem2  9676  cantnfp1lem3  9677  ssttrcl  9712  ttrclselem2  9723  acndom  10048  dfac12lem2  10141  fin23lem14  10330  axcc2lem  10433  pwfseqlem2  10656  uzin  12866  xrmax1  13158  xrmax2  13159  xrmin1  13160  xrmin2  13161  max1ALT  13169  max0sub  13179  ifle  13180  xmulneg1  13252  fzprval  13566  fztpval  13567  modifeq2int  13902  seqf1olem1  14011  seqf1olem2  14012  bcval2  14269  ccatval1  14531  ccatalpha  14547  swrdccat  14689  pfxccat3a  14692  swrdccat3b  14694  repswswrd  14738  cshword  14745  0csh0  14747  ccatco  14790  sgnn  15045  max0add  15261  absmax  15280  sumrblem  15661  fsumcvg  15662  summolem2a  15665  isum  15669  sumss  15674  sumss2  15676  fsumcvg2  15677  fsumser  15680  fsumsplit  15691  sumsplit  15718  prodrblem  15877  fprodcvg  15878  prodmolem2a  15882  zprod  15885  iprod  15886  iprodn0  15888  prodss  15895  fprodsplit  15914  ruclem2  16179  ruclem3  16180  flodddiv4  16360  sadadd2lem2  16395  sadcf  16398  sadc0  16399  sadcp1  16400  sadcaddlem  16402  smupf  16423  smup0  16424  gcd0val  16442  dfgcd2  16492  eucalgf  16524  eucalginv  16525  eucalglt  16526  lcmf0val  16563  phisum  16727  pc0  16791  pcgcd  16815  pcmptcl  16828  pcmpt  16829  pcmpt2  16830  pcprod  16832  fldivp1  16834  prmreclem2  16854  prmreclem4  16856  1arithlem4  16863  vdwlem6  16923  ramtcl2  16948  ramcl2  16953  ramub1lem1  16963  prmop1  16975  fvprmselelfz  16981  fvprmselgcd1  16982  ressid2  17181  xpsfrnel  17512  xpsaddlem  17523  xpsvsca  17527  mreexexd  17596  gsumval1  18608  mgm2nsgrplem2  18836  sgrp2nmndlem2  18841  symgextfve  19328  symgfixfolem1  19347  pmtrmvd  19365  pmtrfinv  19370  pmtrprfval  19396  pmtrprfvalrn  19397  frgpuptinv  19680  frgpup2  19685  frgpup3lem  19686  cyggex  19807  gsumzsplit  19836  gsummpt1n0  19874  dprdfid  19928  dmdprdsplitlem  19948  sdrgacs  20560  abvtrivd  20591  znf1o  21326  uvcvv1  21563  psrlidm  21742  psrridm  21743  mvrf1  21764  mplmonmul  21810  mplcoe1  21811  mplcoe3  21812  mplcoe5  21814  mplmon2  21841  subrgasclcl  21847  evlslem3  21862  evlslem1  21864  coe1tmfv1  22016  ply1sclid  22030  dmatmul  22219  scmatscmiddistr  22230  1mavmul  22270  mulmarep1gsum2  22296  1marepvmarrepid  22297  mdetdiag  22321  mdetralt2  22331  mdetunilem2  22335  mdetunilem7  22340  mdetunilem8  22341  mdetunilem9  22342  mndifsplit  22358  maducoeval2  22362  madugsum  22365  madurid  22366  gsummatr01lem3  22379  gsummatr01  22381  smadiadetglem2  22394  1elcpmat  22437  decpmatid  22492  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  ptpjpre1  23295  ptbasfi  23305  ptpjopn  23336  isfcls  23733  ptcmplem2  23777  ptcmplem3  23778  tsmssplit  23876  dscmet  24301  dscopn  24302  icccmplem2  24559  iccpnfcnv  24684  xrhmeo  24686  pcopt  24762  pcopt2  24763  pcoass  24764  pcorevlem  24766  cmetcaulem  25029  ovolicc1  25257  ioorcl  25318  i1f1lem  25430  itg11  25432  itg1addlem2  25438  itg1addlem4  25440  itg1addlem4OLD  25441  i1fres  25447  itg1climres  25456  mbfi1fseqlem4  25460  mbfi1fseqlem5  25461  mbfi1flim  25465  itg2const2  25483  itg2seq  25484  itg2uba  25485  itg2splitlem  25490  itg2split  25491  itg2monolem1  25492  itg2cnlem1  25503  itg2cnlem2  25504  iblcnlem  25530  iblss  25546  iblss2  25547  itgitg2  25548  itgle  25551  itgss  25553  itgss2  25554  itgss3  25556  itgless  25558  ibladdlem  25561  itgaddlem1  25564  iblabslem  25569  iblabs  25570  iblabsr  25571  iblmulc2  25572  bddmulibl  25580  bddiblnc  25583  itggt0  25585  itgcn  25586  limcvallem  25612  ellimc2  25618  limccnp  25632  limccnp2  25633  limcco  25634  dvcobr  25687  dvexp2  25695  elply2  25934  elplyd  25940  ply1termlem  25941  coe1termlem  25996  abelthlem9  26176  logtayl  26392  leibpilem2  26670  leibpi  26671  rlimcnp2  26695  efrlim  26698  igamz  26776  isnsqf  26863  mule1  26876  sqff1o  26910  muinv  26921  chtublem  26938  dchrelbasd  26966  bposlem1  27011  bposlem3  27013  bposlem5  27015  bposlem6  27016  lgsval2lem  27034  lgsneg  27048  lgsdilem  27051  lgsdir2  27057  lgsdir  27059  lgsdi  27061  lgsne0  27062  gausslemma2dlem1a  27092  2lgslem1c  27120  2lgslem3  27131  2lgs  27134  dchrvmasum2if  27224  dchrvmasumiflem1  27228  rpvmasum2  27239  pntrlog2bndlem4  27307  pntrlog2bndlem5  27308  padicabv  27357  ostth2lem4  27363  nosupno  27430  nosupbday  27432  nosupbnd1  27441  nosupbnd2  27443  noinfno  27445  noinfbday  27447  noinfbnd1  27456  maxs1  27492  maxs2  27493  mins1  27494  mins2  27495  axlowdimlem15  28469  opvtxval  28518  opiedgval  28521  elimifd  32030  elim2if  32031  ifeq3da  32033  ifnefals  32035  pmtridf1o  32511  fzto1stfv1  32518  resvid2  32700  xrge0iifcnv  33199  xrge0iifiso  33201  xrge0iifhom  33203  indval2  33298  ind1  33301  sigaclfu2  33405  ddeval1  33518  eulerpartlemb  33653  ballotlemsima  33800  ballotlemrv1  33805  signsw0glem  33850  signswmnd  33854  signswrid  33855  indispconn  34511  ex-sategoelel  34698  ex-sategoelelomsuc  34703  ex-sategoelel12  34704  mrsubvr  34788  dfrdg2  35059  dfrdg3  35060  unisnif  35189  dfrdg4  35215  gg-dvcobr  35462  fnejoin2  35557  unbdqndv2lem2  35689  bj-xpima2sn  36142  finxpreclem1  36573  finxpreclem3  36577  matunitlindflem1  36787  poimirlem2  36793  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem24  36815  mblfinlem2  36829  mbfposadd  36838  itg2addnclem  36842  itg2gt0cn  36846  ibladdnclem  36847  itgaddnclem1  36849  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  itggt0cn  36861  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  areacirclem5  36883  areacirc  36884  fdc  36916  heiborlem4  36985  ac6s6  37343  cdleme27a  39541  cdleme31sn1  39555  cdleme31fv1  39565  cdlemk40t  40092  dihvalb  40411  sticksstones12a  41279  metakunt5  41295  metakunt6  41296  metakunt10  41300  metakunt11  41301  metakunt20  41310  brif1  41347  brif2  41348  brif12  41349  evlsbagval  41440  selvvvval  41459  fsuppind  41464  dffltz  41678  pw2f1ocnv  42078  aomclem5  42102  kelac1  42107  mon1pid  42249  arearect  42266  areaquad  42267  oe0rif  42337  cantnfresb  42376  safesnsupfidom1o  42470  safesnsupfilb  42471  clsk1indlem1  43098  refsum2cnlem1  44023  upbdrech2  44317  lptioo2  44646  lptioo1  44647  limsupmnfuzlem  44741  limsupre3uzlem  44750  limsup10exlem  44787  coskpi2  44881  cosknegpi  44884  cncfiooicclem1  44908  cncfiooiccre  44910  dvnxpaek  44957  dvnprodlem1  44961  dvnprodlem3  44963  itgioocnicc  44992  iblcncfioo  44993  volico  44998  sublevolico  44999  volioore  45005  voliooico  45007  voliccico  45014  dirkerper  45111  dirkertrigeq  45116  dirkercncflem2  45119  fourierdlem10  45132  fourierdlem32  45154  fourierdlem33  45155  fourierdlem37  45159  fourierdlem62  45183  fourierdlem73  45194  fourierdlem74  45195  fourierdlem75  45196  fourierdlem79  45200  fourierdlem81  45202  fourierdlem82  45203  fourierdlem93  45214  fourierdlem97  45218  fourierdlem101  45222  fourierdlem103  45224  fourierdlem104  45225  sqwvfoura  45243  sqwvfourb  45244  fourierswlem  45245  fouriersw  45246  etransclem4  45253  etransclem15  45264  etransclem19  45268  etransclem20  45269  etransclem23  45272  etransclem24  45273  etransclem25  45274  etransclem27  45276  etransclem31  45280  etransclem32  45281  ioorrnopnxrlem  45321  nnfoctbdjlem  45470  isomenndlem  45545  ovn0val  45565  hoidmv0val  45598  hsphoidmvle2  45600  hoidmv1lelem1  45606  hoidmv1lelem2  45607  hoidmv1le  45609  hoidmvlelem2  45611  hoidmvlelem3  45612  ovnhoilem1  45616  hspdifhsp  45631  hoidifhspdmvle  45635  hspmbllem1  45641  hspmbllem2  45642  hspmbl  45644  volico2  45656  ovnsubadd2lem  45660  ovolval4lem2  45665  ovolval5lem1  45667  afvfundmfveq  46145  dfatafv2iota  46217  dfatafv2eqfv  46268  prproropf1olem3  46472  prproropf1olem4  46473  linc1  47194  lincext3  47225  lindslinindsimp1  47226  el0ldep  47235  islindeps2  47252  itcoval0  47436  ackval0  47454