Theorem iftrue 4491

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2740  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  iftruei  4492  iftrued  4493  iftrueb  4498  ifsb  4499  ifbi  4508  ifeq2da  4518  ifeq12da  4519  ifclda  4521  ifeqda  4522  elimif  4523  ifbothda  4524  ifid  4526  ifeqor  4537  ifnot  4538  ifan  4539  ifor  4540  2if2  4541  dedth  4544  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  dfopif  4833  dfopg  4834  somin1  6131  somincom  6132  xpima1  6180  elimdelov  7512  brif1  7513  ovif12  7516  ifmpt2v  7518  tz7.44-1  8398  rdg0n  8426  resixpfo  8946  boxriin  8950  boxcutc  8951  pw2f1olem  9082  unxpdomlem2  9230  unxpdomlem3  9231  infsupprpr  9479  ordtypelem1  9493  wemaplem2  9522  unwdomg  9559  ixpiunwdom  9565  cantnfp1lem2  9661  cantnfp1lem3  9662  ssttrcl  9697  ttrclselem2  9708  acndom  10057  dfac12lem2  10150  fin23lem14  10338  axcc2lem  10441  pwfseqlem2  10671  indval2  12250  ind1  12254  uzin  12926  xrmax1  13229  xrmax2  13230  xrmin1  13231  xrmin2  13232  max1ALT  13240  max0sub  13250  ifle  13251  xmulneg1  13323  fzprval  13642  fztpval  13643  modifeq2int  13999  seqf1olem1  14107  seqf1olem2  14108  bcval2  14371  tpf1ofv0  14563  tpf1ofv1  14564  ccatval1  14644  ccatalpha  14662  swrdccat  14806  pfxccat3a  14809  swrdccat3b  14811  repswswrd  14857  cshword  14864  0csh0  14866  ccatco  14908  sgnn  15169  max0add  15399  absmax  15419  sumrblem  15799  fsumcvg  15800  summolem2a  15803  isum  15807  sumss  15812  sumss2  15814  fsumcvg2  15815  fsumser  15818  fsumsplit  15829  sumsplit  15856  prodrblem  16020  fprodcvg  16021  prodmolem2a  16025  zprod  16028  iprod  16029  iprodn0  16031  prodss  16038  fprodsplit  16057  ruclem2  16324  ruclem3  16325  flodddiv4  16509  sadadd2lem2  16544  sadcf  16547  sadc0  16548  sadcp1  16549  sadcaddlem  16551  smupf  16572  smup0  16573  gcd0val  16591  dfgcd2  16640  eucalgf  16677  eucalginv  16678  eucalglt  16679  lcmf0val  16716  phisum  16886  pc0  16950  pcgcd  16974  pcmptcl  16987  pcmpt  16988  pcmpt2  16989  pcprod  16991  fldivp1  16993  prmreclem2  17013  prmreclem4  17015  1arithlem4  17022  vdwlem6  17082  ramtcl2  17107  ramcl2  17112  ramub1lem1  17122  prmop1  17134  fvprmselelfz  17140  fvprmselgcd1  17141  ressid2  17330  xpsfrnel  17652  xpsaddlem  17663  xpsvsca  17667  mreexexd  17740  gsumval1  18789  mgm2nsgrplem2  19035  sgrp2nmndlem2  19040  symgextfve  19550  symgfixfolem1  19569  pmtrmvd  19587  pmtrfinv  19592  pmtrprfval  19618  pmtrprfvalrn  19619  frgpuptinv  19902  frgpup2  19907  frgpup3lem  19908  cyggex  20029  gsumzsplit  20058  gsummpt1n0  20096  dprdfid  20150  dmdprdsplitlem  20170  sdrgacs  20971  abvtrivd  21002  znf1o  21768  uvcvv1  22006  psrlidm  22180  psrridm  22181  mvrf1  22204  mplmonmul  22256  mplcoe1  22257  mplcoe3  22258  mplcoe5  22260  mplmon2  22281  subrgasclcl  22287  evlslem3  22300  evlslem1  22302  selvvvval  22362  psdmul  22398  psdmvr  22401  coe1tmfv1  22504  ply1sclid  22518  dmatmul  22723  scmatscmiddistr  22734  1mavmul  22774  mulmarep1gsum2  22800  1marepvmarrepid  22801  mdetdiag  22825  mdetralt2  22835  mdetunilem2  22839  mdetunilem7  22844  mdetunilem8  22845  mdetunilem9  22846  mndifsplit  22862  maducoeval2  22866  madugsum  22869  madurid  22870  gsummatr01lem3  22883  gsummatr01  22885  smadiadetglem2  22898  matunitlindflem1  22905  1elcpmat  22944  decpmatid  22999  chfacfscmulgsum  23089  chfacfpmmulgsum  23093  ptpjpre1  23801  ptbasfi  23811  ptpjopn  23842  isfcls  24239  ptcmplem2  24283  ptcmplem3  24284  tsmssplit  24382  dscmet  24802  dscopn  24803  icccmplem2  25054  iccpnfcnv  25176  xrhmeo  25178  pcopt  25254  pcopt2  25255  pcoass  25256  pcorevlem  25258  cmetcaulem  25520  ovolicc1  25748  ioorcl  25809  i1f1lem  25921  itg11  25923  itg1addlem2  25929  itg1addlem4  25931  i1fres  25937  itg1climres  25946  mbfi1fseqlem4  25950  mbfi1fseqlem5  25951  mbfi1flim  25955  itg2const2  25973  itg2seq  25974  itg2uba  25975  itg2splitlem  25980  itg2split  25981  itg2monolem1  25982  itg2cnlem1  25993  itg2cnlem2  25994  iblcnlem  26021  iblss  26037  iblss2  26038  itgitg2  26039  itgle  26042  itgss  26044  itgss2  26045  itgss3  26047  itgless  26049  ibladdlem  26052  itgaddlem1  26055  iblabslem  26060  iblabs  26061  iblabsr  26062  iblmulc2  26063  bddmulibl  26071  bddiblnc  26074  itggt0  26076  itgcn  26077  limcvallem  26103  ellimc2  26109  limccnp  26123  limccnp2  26124  limcco  26125  dvcobr  26178  dvexp2  26186  mon1pid  26384  elply2  26426  elplyd  26432  ply1termlem  26433  coe1termlem  26488  abelthlem9  26676  logtayl  26898  leibpilem2  27179  leibpi  27180  rlimcnp2  27204  efrlim  27207  igamz  27285  isnsqf  27372  mule1  27385  sqff1o  27419  muinv  27430  chtublem  27448  dchrelbasd  27476  bposlem1  27521  bposlem3  27523  bposlem5  27525  bposlem6  27526  lgsval2lem  27544  lgsneg  27558  lgsdilem  27561  lgsdir2  27567  lgsdir  27569  lgsdi  27571  lgsne0  27572  gausslemma2dlem1a  27602  2lgslem1c  27630  2lgslem3  27641  2lgs  27644  dchrvmasum2if  27734  dchrvmasumiflem1  27738  rpvmasum2  27749  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  padicabv  27867  ostth2lem4  27873  nosupno  27940  nosupbday  27942  nosupbnd1  27951  nosupbnd2  27953  noinfno  27955  noinfbday  27957  noinfbnd1  27966  maxs1  28006  maxs2  28007  mins1  28008  mins2  28009  abssid  28507  abssge0  28511  axlowdimlem15  29414  opvtxval  29461  opiedgval  29464  elimifd  33019  elim2if  33020  ifeq3da  33022  ifnefals  33024  fmptunsnop  33174  pmtridf1o  33536  fzto1stfv1  33543  resvid2  33772  psrmonmul  34062  vieta  34092  2sqr3minply  34292  cos9thpiminply  34300  xrge0iifcnv  34445  xrge0iifiso  34447  xrge0iifhom  34449  sigaclfu2  34633  ddeval1  34747  eulerpartlemb  34881  ballotlemsima  35029  ballotlemrv1  35034  signsw0glem  35063  signswmnd  35067  signswrid  35068  vonf1oonfo  35714  indispconn  35815  ex-sategoelel  36002  ex-sategoelelomsuc  36007  ex-sategoelel12  36008  mrsubvr  36092  dfrdg2  36374  dfrdg3  36375  unisnif  36504  dfrdg4  36532  fnejoin2  36990  unbdqndv2lem2  37209  bj-xpima2sn  37704  finxpreclem1  38145  finxpreclem3  38149  poimirlem2  38373  poimirlem15  38386  poimirlem16  38387  poimirlem17  38388  poimirlem19  38390  poimirlem20  38391  poimirlem24  38395  mblfinlem2  38409  mbfposadd  38418  itg2addnclem  38422  itg2gt0cn  38426  ibladdnclem  38427  itgaddnclem1  38429  iblabsnclem  38434  iblabsnc  38435  iblmulc2nc  38436  itggt0cn  38441  ftc1anclem4  38447  ftc1anclem5  38448  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  areacirclem5  38463  areacirc  38464  fdc  38497  heiborlem4  38566  ac6s6  38922  cdleme27a  41242  cdleme31sn1  41256  cdleme31fv1  41266  cdlemk40t  41793  dihvalb  42112  sticksstones12a  43025  brif2  43096  brif12  43097  evlsbagval  43434  fsuppind  43438  dffltz  43482  pw2f1ocnv  43880  aomclem5  43901  kelac1  43906  arearect  44058  areaquad  44059  oe0rif  44128  cantnfresb  44167  safesnsupfidom1o  44259  safesnsupfilb  44260  clsk1indlem1  44887  refsum2cnlem1  45873  upbdrech2  46143  lptioo2  46463  lptioo1  46464  limsupmnfuzlem  46556  limsupre3uzlem  46565  limsup10exlem  46602  coskpi2  46696  cosknegpi  46699  cncfiooicclem1  46723  cncfiooiccre  46725  dvnxpaek  46772  dvnprodlem1  46776  dvnprodlem3  46778  itgioocnicc  46807  iblcncfioo  46808  volico  46813  sublevolico  46814  volioore  46820  voliooico  46822  voliccico  46829  dirkerper  46926  dirkertrigeq  46931  dirkercncflem2  46934  fourierdlem10  46947  fourierdlem32  46969  fourierdlem33  46970  fourierdlem37  46974  fourierdlem62  46998  fourierdlem73  47009  fourierdlem74  47010  fourierdlem75  47011  fourierdlem79  47015  fourierdlem81  47017  fourierdlem82  47018  fourierdlem93  47029  fourierdlem97  47033  fourierdlem101  47037  fourierdlem103  47039  fourierdlem104  47040  sqwvfoura  47058  sqwvfourb  47059  fourierswlem  47060  fouriersw  47061  etransclem4  47068  etransclem15  47079  etransclem19  47083  etransclem20  47084  etransclem23  47087  etransclem24  47088  etransclem25  47089  etransclem27  47091  etransclem31  47095  etransclem32  47096  ioorrnopnxrlem  47136  nnfoctbdjlem  47285  isomenndlem  47360  ovn0val  47380  hoidmv0val  47413  hsphoidmvle2  47415  hoidmv1lelem1  47421  hoidmv1lelem2  47422  hoidmv1le  47424  hoidmvlelem2  47426  hoidmvlelem3  47427  ovnhoilem1  47431  hspdifhsp  47446  hoidifhspdmvle  47450  hspmbllem1  47456  hspmbllem2  47457  hspmbl  47459  volico2  47471  ovnsubadd2lem  47475  ovolval4lem2  47480  ovolval5lem1  47482  afvfundmfveq  48028  dfatafv2iota  48100  dfatafv2eqfv  48151  difmodm1lt  48255  prproropf1olem3  48407  prproropf1olem4  48408  linc1  49357  lincext3  49388  lindslinindsimp1  49389  el0ldep  49398  islindeps2  49415  itcoval0  49594  ackval0  49612  crosspv1d  50795  crosspv2d  50796  veronesev1lem  50808  veronesev2lem  50809  veronesev3lem  50810  veronesev4lem  50811  veronesev5lem  50812  veronesev6lem  50813  veronesevrowd  50814