Theorem iftrue 4535

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  iftruei  4536  iftrued  4537  ifsb  4542  ifbi  4551  ifeq2da  4561  ifeq12da  4562  ifclda  4564  ifeqda  4565  elimif  4566  ifbothda  4567  ifid  4569  ifeqor  4580  ifnot  4581  ifan  4582  ifor  4583  2if2  4584  dedth  4587  elimhyp  4594  elimhyp2v  4595  elimhyp3v  4596  elimhyp4v  4597  elimdhyp  4599  keephyp2v  4601  keephyp3v  4602  dfopif  4871  dfopg  4872  somin1  6135  somincom  6136  xpima1  6183  elimdelov  7505  ovif12  7508  tz7.44-1  8406  rdg0n  8434  resixpfo  8930  boxriin  8934  boxcutc  8935  pw2f1olem  9076  unxpdomlem2  9251  unxpdomlem3  9252  infsupprpr  9499  ordtypelem1  9513  wemaplem2  9542  unwdomg  9579  ixpiunwdom  9585  cantnfp1lem2  9674  cantnfp1lem3  9675  ssttrcl  9710  ttrclselem2  9721  acndom  10046  dfac12lem2  10139  fin23lem14  10328  axcc2lem  10431  pwfseqlem2  10654  uzin  12862  xrmax1  13154  xrmax2  13155  xrmin1  13156  xrmin2  13157  max1ALT  13165  max0sub  13175  ifle  13176  xmulneg1  13248  fzprval  13562  fztpval  13563  modifeq2int  13898  seqf1olem1  14007  seqf1olem2  14008  bcval2  14265  ccatval1  14527  ccatalpha  14543  swrdccat  14685  pfxccat3a  14688  swrdccat3b  14690  repswswrd  14734  cshword  14741  0csh0  14743  ccatco  14786  sgnn  15041  max0add  15257  absmax  15276  sumrblem  15657  fsumcvg  15658  summolem2a  15661  isum  15665  sumss  15670  sumss2  15672  fsumcvg2  15673  fsumser  15676  fsumsplit  15687  sumsplit  15714  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  iprod  15882  iprodn0  15884  prodss  15891  fprodsplit  15910  ruclem2  16175  ruclem3  16176  flodddiv4  16356  sadadd2lem2  16391  sadcf  16394  sadc0  16395  sadcp1  16396  sadcaddlem  16398  smupf  16419  smup0  16420  gcd0val  16438  dfgcd2  16488  eucalgf  16520  eucalginv  16521  eucalglt  16522  lcmf0val  16559  phisum  16723  pc0  16787  pcgcd  16811  pcmptcl  16824  pcmpt  16825  pcmpt2  16826  pcprod  16828  fldivp1  16830  prmreclem2  16850  prmreclem4  16852  1arithlem4  16859  vdwlem6  16919  ramtcl2  16944  ramcl2  16949  ramub1lem1  16959  prmop1  16971  fvprmselelfz  16977  fvprmselgcd1  16978  ressid2  17177  xpsfrnel  17508  xpsaddlem  17519  xpsvsca  17523  mreexexd  17592  gsumval1  18602  mgm2nsgrplem2  18800  sgrp2nmndlem2  18805  symgextfve  19287  symgfixfolem1  19306  pmtrmvd  19324  pmtrfinv  19329  pmtrprfval  19355  pmtrprfvalrn  19356  frgpuptinv  19639  frgpup2  19644  frgpup3lem  19645  cyggex  19766  gsumzsplit  19795  gsummpt1n0  19833  dprdfid  19887  dmdprdsplitlem  19907  sdrgacs  20417  abvtrivd  20448  znf1o  21107  uvcvv1  21344  psrlidm  21523  psrridm  21524  mvrf1  21545  mplmonmul  21591  mplcoe1  21592  mplcoe3  21593  mplcoe5  21595  mplmon2  21622  subrgasclcl  21628  evlslem3  21643  evlslem1  21645  coe1tmfv1  21796  ply1sclid  21810  dmatmul  21999  scmatscmiddistr  22010  1mavmul  22050  mulmarep1gsum2  22076  1marepvmarrepid  22077  mdetdiag  22101  mdetralt2  22111  mdetunilem2  22115  mdetunilem7  22120  mdetunilem8  22121  mdetunilem9  22122  mndifsplit  22138  maducoeval2  22142  madugsum  22145  madurid  22146  gsummatr01lem3  22159  gsummatr01  22161  smadiadetglem2  22174  1elcpmat  22217  decpmatid  22272  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  ptpjpre1  23075  ptbasfi  23085  ptpjopn  23116  isfcls  23513  ptcmplem2  23557  ptcmplem3  23558  tsmssplit  23656  dscmet  24081  dscopn  24082  icccmplem2  24339  iccpnfcnv  24460  xrhmeo  24462  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  cmetcaulem  24805  ovolicc1  25033  ioorcl  25094  i1f1lem  25206  itg11  25208  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1flim  25241  itg2const2  25259  itg2seq  25260  itg2uba  25261  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2cnlem1  25279  itg2cnlem2  25280  iblcnlem  25306  iblss  25322  iblss2  25323  itgitg2  25324  itgle  25327  itgss  25329  itgss2  25330  itgss3  25332  itgless  25334  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  bddmulibl  25356  bddiblnc  25359  itggt0  25361  itgcn  25362  limcvallem  25388  ellimc2  25394  limccnp  25408  limccnp2  25409  limcco  25410  dvcobr  25463  dvexp2  25471  elply2  25710  elplyd  25716  ply1termlem  25717  coe1termlem  25772  abelthlem9  25952  logtayl  26168  leibpilem2  26446  leibpi  26447  rlimcnp2  26471  efrlim  26474  igamz  26552  isnsqf  26639  mule1  26652  sqff1o  26686  muinv  26697  chtublem  26714  dchrelbasd  26742  bposlem1  26787  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgsval2lem  26810  lgsneg  26824  lgsdilem  26827  lgsdir2  26833  lgsdir  26835  lgsdi  26837  lgsne0  26838  gausslemma2dlem1a  26868  2lgslem1c  26896  2lgslem3  26907  2lgs  26910  dchrvmasum2if  27000  dchrvmasumiflem1  27004  rpvmasum2  27015  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  padicabv  27133  ostth2lem4  27139  nosupno  27206  nosupbday  27208  nosupbnd1  27217  nosupbnd2  27219  noinfno  27221  noinfbday  27223  noinfbnd1  27232  maxs1  27268  maxs2  27269  mins1  27270  mins2  27271  axlowdimlem15  28245  opvtxval  28294  opiedgval  28297  elimifd  31806  elim2if  31807  ifeq3da  31809  ifnefals  31811  pmtridf1o  32284  fzto1stfv1  32291  resvid2  32473  xrge0iifcnv  32944  xrge0iifiso  32946  xrge0iifhom  32948  indval2  33043  ind1  33046  sigaclfu2  33150  ddeval1  33263  eulerpartlemb  33398  ballotlemsima  33545  ballotlemrv1  33550  signsw0glem  33595  signswmnd  33599  signswrid  33600  indispconn  34256  ex-sategoelel  34443  ex-sategoelelomsuc  34448  ex-sategoelel12  34449  mrsubvr  34533  dfrdg2  34798  dfrdg3  34799  unisnif  34928  dfrdg4  34954  gg-dvcobr  35207  fnejoin2  35302  unbdqndv2lem2  35434  bj-xpima2sn  35887  finxpreclem1  36318  finxpreclem3  36322  matunitlindflem1  36532  poimirlem2  36538  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem24  36560  mblfinlem2  36574  mbfposadd  36583  itg2addnclem  36587  itg2gt0cn  36591  ibladdnclem  36592  itgaddnclem1  36594  iblabsnclem  36599  iblabsnc  36600  iblmulc2nc  36601  itggt0cn  36606  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  areacirclem5  36628  areacirc  36629  fdc  36661  heiborlem4  36730  ac6s6  37088  cdleme27a  39286  cdleme31sn1  39300  cdleme31fv1  39310  cdlemk40t  39837  dihvalb  40156  sticksstones12a  41021  metakunt5  41037  metakunt6  41038  metakunt10  41042  metakunt11  41043  metakunt20  41052  brif1  41089  brif2  41090  brif12  41091  evlsbagval  41186  selvvvval  41205  fsuppind  41210  dffltz  41424  pw2f1ocnv  41824  aomclem5  41848  kelac1  41853  mon1pid  41995  arearect  42012  areaquad  42013  oe0rif  42083  cantnfresb  42122  safesnsupfidom1o  42216  safesnsupfilb  42217  clsk1indlem1  42844  refsum2cnlem1  43769  upbdrech2  44066  lptioo2  44395  lptioo1  44396  limsupmnfuzlem  44490  limsupre3uzlem  44499  limsup10exlem  44536  coskpi2  44630  cosknegpi  44633  cncfiooicclem1  44657  cncfiooiccre  44659  dvnxpaek  44706  dvnprodlem1  44710  dvnprodlem3  44712  itgioocnicc  44741  iblcncfioo  44742  volico  44747  sublevolico  44748  volioore  44754  voliooico  44756  voliccico  44763  dirkerper  44860  dirkertrigeq  44865  dirkercncflem2  44868  fourierdlem10  44881  fourierdlem32  44903  fourierdlem33  44904  fourierdlem37  44908  fourierdlem62  44932  fourierdlem73  44943  fourierdlem74  44944  fourierdlem75  44945  fourierdlem79  44949  fourierdlem81  44951  fourierdlem82  44952  fourierdlem93  44963  fourierdlem97  44967  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  sqwvfoura  44992  sqwvfourb  44993  fourierswlem  44994  fouriersw  44995  etransclem4  45002  etransclem15  45013  etransclem19  45017  etransclem20  45018  etransclem23  45021  etransclem24  45022  etransclem25  45023  etransclem27  45025  etransclem31  45029  etransclem32  45030  ioorrnopnxrlem  45070  nnfoctbdjlem  45219  isomenndlem  45294  ovn0val  45314  hoidmv0val  45347  hsphoidmvle2  45349  hoidmv1lelem1  45355  hoidmv1lelem2  45356  hoidmv1le  45358  hoidmvlelem2  45360  hoidmvlelem3  45361  ovnhoilem1  45365  hspdifhsp  45380  hoidifhspdmvle  45384  hspmbllem1  45390  hspmbllem2  45391  hspmbl  45393  volico2  45405  ovnsubadd2lem  45409  ovolval4lem2  45414  ovolval5lem1  45416  afvfundmfveq  45894  dfatafv2iota  45966  dfatafv2eqfv  46017  prproropf1olem3  46221  prproropf1olem4  46222  linc1  47154  lincext3  47185  lindslinindsimp1  47186  el0ldep  47195  islindeps2  47212  itcoval0  47396  ackval0  47414