Theorem iftrue 4473

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4467

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  iftruei  4474  iftrued  4475  iftrueb  4480  ifsb  4481  ifbi  4490  ifeq2da  4500  ifeq12da  4501  ifclda  4503  ifeqda  4504  elimif  4505  ifbothda  4506  ifid  4508  ifeqor  4519  ifnot  4520  ifan  4521  ifor  4522  2if2  4523  dedth  4526  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elimdhyp  4538  keephyp2v  4540  keephyp3v  4541  dfopif  4814  dfopg  4815  somin1  6097  somincom  6098  xpima1  6148  elimdelov  7463  brif1  7464  ovif12  7467  ifmpt2v  7469  tz7.44-1  8345  rdg0n  8373  resixpfo  8884  boxriin  8888  boxcutc  8889  pw2f1olem  9019  unxpdomlem2  9167  unxpdomlem3  9168  infsupprpr  9419  ordtypelem1  9433  wemaplem2  9462  unwdomg  9499  ixpiunwdom  9505  cantnfp1lem2  9600  cantnfp1lem3  9601  ssttrcl  9636  ttrclselem2  9647  acndom  9973  dfac12lem2  10067  fin23lem14  10255  axcc2lem  10358  pwfseqlem2  10582  indval2  12164  ind1  12168  uzin  12824  xrmax1  13127  xrmax2  13128  xrmin1  13129  xrmin2  13130  max1ALT  13138  max0sub  13148  ifle  13149  xmulneg1  13221  fzprval  13539  fztpval  13540  modifeq2int  13895  seqf1olem1  14003  seqf1olem2  14004  bcval2  14267  tpf1ofv0  14458  tpf1ofv1  14459  ccatval1  14539  ccatalpha  14556  swrdccat  14697  pfxccat3a  14700  swrdccat3b  14702  repswswrd  14746  cshword  14753  0csh0  14755  ccatco  14797  sgnn  15056  max0add  15272  absmax  15292  sumrblem  15673  fsumcvg  15674  summolem2a  15677  isum  15681  sumss  15686  sumss2  15688  fsumcvg2  15689  fsumser  15692  fsumsplit  15703  sumsplit  15730  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  zprod  15902  iprod  15903  iprodn0  15905  prodss  15912  fprodsplit  15931  ruclem2  16199  ruclem3  16200  flodddiv4  16384  sadadd2lem2  16419  sadcf  16422  sadc0  16423  sadcp1  16424  sadcaddlem  16426  smupf  16447  smup0  16448  gcd0val  16466  dfgcd2  16515  eucalgf  16552  eucalginv  16553  eucalglt  16554  lcmf0val  16591  phisum  16761  pc0  16825  pcgcd  16849  pcmptcl  16862  pcmpt  16863  pcmpt2  16864  pcprod  16866  fldivp1  16868  prmreclem2  16888  prmreclem4  16890  1arithlem4  16897  vdwlem6  16957  ramtcl2  16982  ramcl2  16987  ramub1lem1  16997  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  ressid2  17204  xpsfrnel  17526  xpsaddlem  17537  xpsvsca  17541  mreexexd  17614  gsumval1  18651  mgm2nsgrplem2  18890  sgrp2nmndlem2  18895  symgextfve  19394  symgfixfolem1  19413  pmtrmvd  19431  pmtrfinv  19436  pmtrprfval  19462  pmtrprfvalrn  19463  frgpuptinv  19746  frgpup2  19751  frgpup3lem  19752  cyggex  19873  gsumzsplit  19902  gsummpt1n0  19940  dprdfid  19994  dmdprdsplitlem  20014  sdrgacs  20778  abvtrivd  20809  znf1o  21531  uvcvv1  21769  psrlidm  21940  psrridm  21941  mvrf1  21964  mplmonmul  22014  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  mplmon2  22039  subrgasclcl  22045  evlslem3  22058  evlslem1  22060  psdmul  22132  psdmvr  22135  coe1tmfv1  22239  ply1sclid  22253  dmatmul  22462  scmatscmiddistr  22473  1mavmul  22513  mulmarep1gsum2  22539  1marepvmarrepid  22540  mdetdiag  22564  mdetralt2  22574  mdetunilem2  22578  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  mndifsplit  22601  maducoeval2  22605  madugsum  22608  madurid  22609  gsummatr01lem3  22622  gsummatr01  22624  smadiadetglem2  22637  1elcpmat  22680  decpmatid  22735  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  ptpjpre1  23536  ptbasfi  23546  ptpjopn  23577  isfcls  23974  ptcmplem2  24018  ptcmplem3  24019  tsmssplit  24117  dscmet  24537  dscopn  24538  icccmplem2  24789  iccpnfcnv  24911  xrhmeo  24913  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  cmetcaulem  25255  ovolicc1  25483  ioorcl  25544  i1f1lem  25656  itg11  25658  itg1addlem2  25664  itg1addlem4  25666  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1flim  25690  itg2const2  25708  itg2seq  25709  itg2uba  25710  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2cnlem1  25728  itg2cnlem2  25729  iblcnlem  25756  iblss  25772  iblss2  25773  itgitg2  25774  itgle  25777  itgss  25779  itgss2  25780  itgss3  25782  itgless  25784  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  bddmulibl  25806  bddiblnc  25809  itggt0  25811  itgcn  25812  limcvallem  25838  ellimc2  25844  limccnp  25858  limccnp2  25859  limcco  25860  dvcobr  25913  dvexp2  25921  mon1pid  26119  elply2  26161  elplyd  26167  ply1termlem  26168  coe1termlem  26223  abelthlem9  26405  logtayl  26624  leibpilem2  26905  leibpi  26906  rlimcnp2  26930  efrlim  26933  igamz  27011  isnsqf  27098  mule1  27111  sqff1o  27145  muinv  27156  chtublem  27174  dchrelbasd  27202  bposlem1  27247  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgsval2lem  27270  lgsneg  27284  lgsdilem  27287  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsne0  27298  gausslemma2dlem1a  27328  2lgslem1c  27356  2lgslem3  27367  2lgs  27370  dchrvmasum2if  27460  dchrvmasumiflem1  27464  rpvmasum2  27475  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  padicabv  27593  ostth2lem4  27599  nosupno  27667  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1  27693  maxs1  27733  maxs2  27734  mins1  27735  mins2  27736  abssid  28233  abssge0  28237  axlowdimlem15  29025  opvtxval  29072  opiedgval  29075  elimifd  32613  elim2if  32614  ifeq3da  32616  ifnefals  32618  fmptunsnop  32773  pmtridf1o  33155  fzto1stfv1  33162  resvid2  33390  psrmonmul  33694  vieta  33724  2sqr3minply  33924  cos9thpiminply  33932  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  sigaclfu2  34265  ddeval1  34378  eulerpartlemb  34512  ballotlemsima  34660  ballotlemrv1  34665  signsw0glem  34697  signswmnd  34701  signswrid  34702  indispconn  35416  ex-sategoelel  35603  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  mrsubvr  35693  dfrdg2  35975  dfrdg3  35976  unisnif  36105  dfrdg4  36133  fnejoin2  36551  unbdqndv2lem2  36770  bj-xpima2sn  37265  finxpreclem1  37705  finxpreclem3  37709  matunitlindflem1  37937  poimirlem2  37943  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  mblfinlem2  37979  mbfposadd  37988  itg2addnclem  37992  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itggt0cn  38011  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem5  38033  areacirc  38034  fdc  38066  heiborlem4  38135  ac6s6  38493  cdleme27a  40813  cdleme31sn1  40827  cdleme31fv1  40837  cdlemk40t  41364  dihvalb  41683  sticksstones12a  42596  brif2  42665  brif12  42666  evlsbagval  43002  selvvvval  43018  fsuppind  43023  dffltz  43067  pw2f1ocnv  43465  aomclem5  43486  kelac1  43491  arearect  43643  areaquad  43644  oe0rif  43713  cantnfresb  43752  safesnsupfidom1o  43844  safesnsupfilb  43845  clsk1indlem1  44472  refsum2cnlem1  45468  upbdrech2  45741  lptioo2  46061  lptioo1  46062  limsupmnfuzlem  46154  limsupre3uzlem  46163  limsup10exlem  46200  coskpi2  46294  cosknegpi  46297  cncfiooicclem1  46321  cncfiooiccre  46323  dvnxpaek  46370  dvnprodlem1  46374  dvnprodlem3  46376  itgioocnicc  46405  iblcncfioo  46406  volico  46411  sublevolico  46412  volioore  46418  voliooico  46420  voliccico  46427  dirkerper  46524  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem10  46545  fourierdlem32  46567  fourierdlem33  46568  fourierdlem37  46572  fourierdlem62  46596  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem4  46666  etransclem15  46677  etransclem19  46681  etransclem20  46682  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem27  46689  etransclem31  46693  etransclem32  46694  ioorrnopnxrlem  46734  nnfoctbdjlem  46883  isomenndlem  46958  ovn0val  46978  hoidmv0val  47011  hsphoidmvle2  47013  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  hspdifhsp  47044  hoidifhspdmvle  47048  hspmbllem1  47054  hspmbllem2  47055  hspmbl  47057  volico2  47069  ovnsubadd2lem  47073  ovolval4lem2  47078  ovolval5lem1  47080  afvfundmfveq  47580  dfatafv2iota  47652  dfatafv2eqfv  47703  difmodm1lt  47807  prproropf1olem3  47959  prproropf1olem4  47960  linc1  48895  lincext3  48926  lindslinindsimp1  48927  el0ldep  48936  islindeps2  48953  itcoval0  49132  ackval0  49150