Theorem iftrue 4530

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  {cab 2704  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-if 4525

This theorem is referenced by:  iftruei  4531  iftrued  4532  ifsb  4537  ifbi  4546  ifeq2da  4556  ifeq12da  4557  ifclda  4559  ifeqda  4560  elimif  4561  ifbothda  4562  ifid  4564  ifeqor  4575  ifnot  4576  ifan  4577  ifor  4578  2if2  4579  dedth  4582  elimhyp  4589  elimhyp2v  4590  elimhyp3v  4591  elimhyp4v  4592  elimdhyp  4594  keephyp2v  4596  keephyp3v  4597  dfopif  4866  dfopg  4867  somin1  6133  somincom  6134  xpima1  6181  elimdelov  7510  brif1  7511  ovif12  7514  tz7.44-1  8420  rdg0n  8448  resixpfo  8948  boxriin  8952  boxcutc  8953  pw2f1olem  9094  unxpdomlem2  9269  unxpdomlem3  9270  infsupprpr  9521  ordtypelem1  9535  wemaplem2  9564  unwdomg  9601  ixpiunwdom  9607  cantnfp1lem2  9696  cantnfp1lem3  9697  ssttrcl  9732  ttrclselem2  9743  acndom  10068  dfac12lem2  10161  fin23lem14  10350  axcc2lem  10453  pwfseqlem2  10676  uzin  12886  xrmax1  13180  xrmax2  13181  xrmin1  13182  xrmin2  13183  max1ALT  13191  max0sub  13201  ifle  13202  xmulneg1  13274  fzprval  13588  fztpval  13589  modifeq2int  13924  seqf1olem1  14032  seqf1olem2  14033  bcval2  14290  ccatval1  14553  ccatalpha  14569  swrdccat  14711  pfxccat3a  14714  swrdccat3b  14716  repswswrd  14760  cshword  14767  0csh0  14769  ccatco  14812  sgnn  15067  max0add  15283  absmax  15302  sumrblem  15683  fsumcvg  15684  summolem2a  15687  isum  15691  sumss  15696  sumss2  15698  fsumcvg2  15699  fsumser  15702  fsumsplit  15713  sumsplit  15740  prodrblem  15899  fprodcvg  15900  prodmolem2a  15904  zprod  15907  iprod  15908  iprodn0  15910  prodss  15917  fprodsplit  15936  ruclem2  16202  ruclem3  16203  flodddiv4  16383  sadadd2lem2  16418  sadcf  16421  sadc0  16422  sadcp1  16423  sadcaddlem  16425  smupf  16446  smup0  16447  gcd0val  16465  dfgcd2  16515  eucalgf  16547  eucalginv  16548  eucalglt  16549  lcmf0val  16586  phisum  16752  pc0  16816  pcgcd  16840  pcmptcl  16853  pcmpt  16854  pcmpt2  16855  pcprod  16857  fldivp1  16859  prmreclem2  16879  prmreclem4  16881  1arithlem4  16888  vdwlem6  16948  ramtcl2  16973  ramcl2  16978  ramub1lem1  16988  prmop1  17000  fvprmselelfz  17006  fvprmselgcd1  17007  ressid2  17206  xpsfrnel  17537  xpsaddlem  17548  xpsvsca  17552  mreexexd  17621  gsumval1  18636  mgm2nsgrplem2  18864  sgrp2nmndlem2  18869  symgextfve  19367  symgfixfolem1  19386  pmtrmvd  19404  pmtrfinv  19409  pmtrprfval  19435  pmtrprfvalrn  19436  frgpuptinv  19719  frgpup2  19724  frgpup3lem  19725  cyggex  19846  gsumzsplit  19875  gsummpt1n0  19913  dprdfid  19967  dmdprdsplitlem  19987  sdrgacs  20682  abvtrivd  20713  znf1o  21478  uvcvv1  21716  psrlidm  21898  psrridm  21899  mvrf1  21921  mplmonmul  21967  mplcoe1  21968  mplcoe3  21969  mplcoe5  21971  mplmon2  21998  subrgasclcl  22004  evlslem3  22019  evlslem1  22021  psdmul  22083  coe1tmfv1  22186  ply1sclid  22200  dmatmul  22392  scmatscmiddistr  22403  1mavmul  22443  mulmarep1gsum2  22469  1marepvmarrepid  22470  mdetdiag  22494  mdetralt2  22504  mdetunilem2  22508  mdetunilem7  22513  mdetunilem8  22514  mdetunilem9  22515  mndifsplit  22531  maducoeval2  22535  madugsum  22538  madurid  22539  gsummatr01lem3  22552  gsummatr01  22554  smadiadetglem2  22567  1elcpmat  22610  decpmatid  22665  chfacfscmulgsum  22755  chfacfpmmulgsum  22759  ptpjpre1  23468  ptbasfi  23478  ptpjopn  23509  isfcls  23906  ptcmplem2  23950  ptcmplem3  23951  tsmssplit  24049  dscmet  24474  dscopn  24475  icccmplem2  24732  iccpnfcnv  24862  xrhmeo  24864  pcopt  24942  pcopt2  24943  pcoass  24944  pcorevlem  24946  cmetcaulem  25209  ovolicc1  25438  ioorcl  25499  i1f1lem  25611  itg11  25613  itg1addlem2  25619  itg1addlem4  25621  itg1addlem4OLD  25622  i1fres  25628  itg1climres  25637  mbfi1fseqlem4  25641  mbfi1fseqlem5  25642  mbfi1flim  25646  itg2const2  25664  itg2seq  25665  itg2uba  25666  itg2splitlem  25671  itg2split  25672  itg2monolem1  25673  itg2cnlem1  25684  itg2cnlem2  25685  iblcnlem  25711  iblss  25727  iblss2  25728  itgitg2  25729  itgle  25732  itgss  25734  itgss2  25735  itgss3  25737  itgless  25739  ibladdlem  25742  itgaddlem1  25745  iblabslem  25750  iblabs  25751  iblabsr  25752  iblmulc2  25753  bddmulibl  25761  bddiblnc  25764  itggt0  25766  itgcn  25767  limcvallem  25793  ellimc2  25799  limccnp  25813  limccnp2  25814  limcco  25815  dvcobr  25870  dvcobrOLD  25871  dvexp2  25879  mon1pid  26082  elply2  26123  elplyd  26129  ply1termlem  26130  coe1termlem  26185  abelthlem9  26370  logtayl  26587  leibpilem2  26866  leibpi  26867  rlimcnp2  26891  efrlim  26894  efrlimOLD  26895  igamz  26973  isnsqf  27060  mule1  27073  sqff1o  27107  muinv  27118  chtublem  27137  dchrelbasd  27165  bposlem1  27210  bposlem3  27212  bposlem5  27214  bposlem6  27215  lgsval2lem  27233  lgsneg  27247  lgsdilem  27250  lgsdir2  27256  lgsdir  27258  lgsdi  27260  lgsne0  27261  gausslemma2dlem1a  27291  2lgslem1c  27319  2lgslem3  27330  2lgs  27333  dchrvmasum2if  27423  dchrvmasumiflem1  27427  rpvmasum2  27438  pntrlog2bndlem4  27506  pntrlog2bndlem5  27507  padicabv  27556  ostth2lem4  27562  nosupno  27629  nosupbday  27631  nosupbnd1  27640  nosupbnd2  27642  noinfno  27644  noinfbday  27646  noinfbnd1  27655  maxs1  27691  maxs2  27692  mins1  27693  mins2  27694  abssid  28128  abssge0  28132  axlowdimlem15  28760  opvtxval  28809  opiedgval  28812  elimifd  32327  elim2if  32328  ifeq3da  32330  ifnefals  32332  pmtridf1o  32809  fzto1stfv1  32816  resvid2  33033  xrge0iifcnv  33524  xrge0iifiso  33526  xrge0iifhom  33528  indval2  33623  ind1  33626  sigaclfu2  33730  ddeval1  33843  eulerpartlemb  33978  ballotlemsima  34125  ballotlemrv1  34130  signsw0glem  34175  signswmnd  34179  signswrid  34180  indispconn  34834  ex-sategoelel  35021  ex-sategoelelomsuc  35026  ex-sategoelel12  35027  mrsubvr  35111  dfrdg2  35381  dfrdg3  35382  unisnif  35511  dfrdg4  35537  fnejoin2  35843  unbdqndv2lem2  35975  bj-xpima2sn  36427  finxpreclem1  36858  finxpreclem3  36862  matunitlindflem1  37078  poimirlem2  37084  poimirlem15  37097  poimirlem16  37098  poimirlem17  37099  poimirlem19  37101  poimirlem20  37102  poimirlem24  37106  mblfinlem2  37120  mbfposadd  37129  itg2addnclem  37133  itg2gt0cn  37137  ibladdnclem  37138  itgaddnclem1  37140  iblabsnclem  37145  iblabsnc  37146  iblmulc2nc  37147  itggt0cn  37152  ftc1anclem4  37158  ftc1anclem5  37159  ftc1anclem6  37160  ftc1anclem7  37161  ftc1anclem8  37162  ftc1anc  37163  areacirclem5  37174  areacirc  37175  fdc  37207  heiborlem4  37276  ac6s6  37634  cdleme27a  39829  cdleme31sn1  39843  cdleme31fv1  39853  cdlemk40t  40380  dihvalb  40699  sticksstones12a  41613  metakunt5  41633  metakunt6  41634  metakunt10  41638  metakunt11  41639  metakunt20  41648  brif2  41684  brif12  41685  evlsbagval  41771  selvvvval  41790  fsuppind  41795  dffltz  42030  pw2f1ocnv  42430  aomclem5  42454  kelac1  42459  arearect  42615  areaquad  42616  oe0rif  42686  cantnfresb  42725  safesnsupfidom1o  42819  safesnsupfilb  42820  clsk1indlem1  43447  refsum2cnlem1  44371  upbdrech2  44662  lptioo2  44991  lptioo1  44992  limsupmnfuzlem  45086  limsupre3uzlem  45095  limsup10exlem  45132  coskpi2  45226  cosknegpi  45229  cncfiooicclem1  45253  cncfiooiccre  45255  dvnxpaek  45302  dvnprodlem1  45306  dvnprodlem3  45308  itgioocnicc  45337  iblcncfioo  45338  volico  45343  sublevolico  45344  volioore  45350  voliooico  45352  voliccico  45359  dirkerper  45456  dirkertrigeq  45461  dirkercncflem2  45464  fourierdlem10  45477  fourierdlem32  45499  fourierdlem33  45500  fourierdlem37  45504  fourierdlem62  45528  fourierdlem73  45539  fourierdlem74  45540  fourierdlem75  45541  fourierdlem79  45545  fourierdlem81  45547  fourierdlem82  45548  fourierdlem93  45559  fourierdlem97  45563  fourierdlem101  45567  fourierdlem103  45569  fourierdlem104  45570  sqwvfoura  45588  sqwvfourb  45589  fourierswlem  45590  fouriersw  45591  etransclem4  45598  etransclem15  45609  etransclem19  45613  etransclem20  45614  etransclem23  45617  etransclem24  45618  etransclem25  45619  etransclem27  45621  etransclem31  45625  etransclem32  45626  ioorrnopnxrlem  45666  nnfoctbdjlem  45815  isomenndlem  45890  ovn0val  45910  hoidmv0val  45943  hsphoidmvle2  45945  hoidmv1lelem1  45951  hoidmv1lelem2  45952  hoidmv1le  45954  hoidmvlelem2  45956  hoidmvlelem3  45957  ovnhoilem1  45961  hspdifhsp  45976  hoidifhspdmvle  45980  hspmbllem1  45986  hspmbllem2  45987  hspmbl  45989  volico2  46001  ovnsubadd2lem  46005  ovolval4lem2  46010  ovolval5lem1  46012  afvfundmfveq  46490  dfatafv2iota  46562  dfatafv2eqfv  46613  prproropf1olem3  46817  prproropf1olem4  46818  linc1  47465  lincext3  47496  lindslinindsimp1  47497  el0ldep  47506  islindeps2  47523  itcoval0  47707  ackval0  47725