Theorem iftrue 4531

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  iftruei  4532  iftrued  4533  iftrueb  4538  ifsb  4539  ifbi  4548  ifeq2da  4558  ifeq12da  4559  ifclda  4561  ifeqda  4562  elimif  4563  ifbothda  4564  ifid  4566  ifeqor  4577  ifnot  4578  ifan  4579  ifor  4580  2if2  4581  dedth  4584  elimhyp  4591  elimhyp2v  4592  elimhyp3v  4593  elimhyp4v  4594  elimdhyp  4596  keephyp2v  4598  keephyp3v  4599  dfopif  4870  dfopg  4871  somin1  6153  somincom  6154  xpima1  6203  elimdelov  7529  brif1  7530  ovif12  7533  ifmpt2v  7535  tz7.44-1  8446  rdg0n  8474  resixpfo  8976  boxriin  8980  boxcutc  8981  pw2f1olem  9116  unxpdomlem2  9287  unxpdomlem3  9288  infsupprpr  9544  ordtypelem1  9558  wemaplem2  9587  unwdomg  9624  ixpiunwdom  9630  cantnfp1lem2  9719  cantnfp1lem3  9720  ssttrcl  9755  ttrclselem2  9766  acndom  10091  dfac12lem2  10185  fin23lem14  10373  axcc2lem  10476  pwfseqlem2  10699  uzin  12918  xrmax1  13217  xrmax2  13218  xrmin1  13219  xrmin2  13220  max1ALT  13228  max0sub  13238  ifle  13239  xmulneg1  13311  fzprval  13625  fztpval  13626  modifeq2int  13974  seqf1olem1  14082  seqf1olem2  14083  bcval2  14344  tpf1ofv0  14535  tpf1ofv1  14536  ccatval1  14615  ccatalpha  14631  swrdccat  14773  pfxccat3a  14776  swrdccat3b  14778  repswswrd  14822  cshword  14829  0csh0  14831  ccatco  14874  sgnn  15133  max0add  15349  absmax  15368  sumrblem  15747  fsumcvg  15748  summolem2a  15751  isum  15755  sumss  15760  sumss2  15762  fsumcvg2  15763  fsumser  15766  fsumsplit  15777  sumsplit  15804  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  iprod  15974  iprodn0  15976  prodss  15983  fprodsplit  16002  ruclem2  16268  ruclem3  16269  flodddiv4  16452  sadadd2lem2  16487  sadcf  16490  sadc0  16491  sadcp1  16492  sadcaddlem  16494  smupf  16515  smup0  16516  gcd0val  16534  dfgcd2  16583  eucalgf  16620  eucalginv  16621  eucalglt  16622  lcmf0val  16659  phisum  16828  pc0  16892  pcgcd  16916  pcmptcl  16929  pcmpt  16930  pcmpt2  16931  pcprod  16933  fldivp1  16935  prmreclem2  16955  prmreclem4  16957  1arithlem4  16964  vdwlem6  17024  ramtcl2  17049  ramcl2  17054  ramub1lem1  17064  prmop1  17076  fvprmselelfz  17082  fvprmselgcd1  17083  ressid2  17278  xpsfrnel  17607  xpsaddlem  17618  xpsvsca  17622  mreexexd  17691  gsumval1  18696  mgm2nsgrplem2  18932  sgrp2nmndlem2  18937  symgextfve  19437  symgfixfolem1  19456  pmtrmvd  19474  pmtrfinv  19479  pmtrprfval  19505  pmtrprfvalrn  19506  frgpuptinv  19789  frgpup2  19794  frgpup3lem  19795  cyggex  19916  gsumzsplit  19945  gsummpt1n0  19983  dprdfid  20037  dmdprdsplitlem  20057  sdrgacs  20802  abvtrivd  20833  znf1o  21570  uvcvv1  21809  psrlidm  21982  psrridm  21983  mvrf1  22006  mplmonmul  22054  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  mplmon2  22085  subrgasclcl  22091  evlslem3  22104  evlslem1  22106  psdmul  22170  psdmvr  22173  coe1tmfv1  22277  ply1sclid  22291  dmatmul  22503  scmatscmiddistr  22514  1mavmul  22554  mulmarep1gsum2  22580  1marepvmarrepid  22581  mdetdiag  22605  mdetralt2  22615  mdetunilem2  22619  mdetunilem7  22624  mdetunilem8  22625  mdetunilem9  22626  mndifsplit  22642  maducoeval2  22646  madugsum  22649  madurid  22650  gsummatr01lem3  22663  gsummatr01  22665  smadiadetglem2  22678  1elcpmat  22721  decpmatid  22776  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  ptpjpre1  23579  ptbasfi  23589  ptpjopn  23620  isfcls  24017  ptcmplem2  24061  ptcmplem3  24062  tsmssplit  24160  dscmet  24585  dscopn  24586  icccmplem2  24845  iccpnfcnv  24975  xrhmeo  24977  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  cmetcaulem  25322  ovolicc1  25551  ioorcl  25612  i1f1lem  25724  itg11  25726  itg1addlem2  25732  itg1addlem4  25734  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1flim  25758  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2cnlem1  25796  itg2cnlem2  25797  iblcnlem  25824  iblss  25840  iblss2  25841  itgitg2  25842  itgle  25845  itgss  25847  itgss2  25848  itgss3  25850  itgless  25852  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddmulibl  25874  bddiblnc  25877  itggt0  25879  itgcn  25880  limcvallem  25906  ellimc2  25912  limccnp  25926  limccnp2  25927  limcco  25928  dvcobr  25983  dvcobrOLD  25984  dvexp2  25992  mon1pid  26193  elply2  26235  elplyd  26241  ply1termlem  26242  coe1termlem  26297  abelthlem9  26484  logtayl  26702  leibpilem2  26984  leibpi  26985  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  igamz  27091  isnsqf  27178  mule1  27191  sqff1o  27225  muinv  27236  chtublem  27255  dchrelbasd  27283  bposlem1  27328  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgsval2lem  27351  lgsneg  27365  lgsdilem  27368  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsne0  27379  gausslemma2dlem1a  27409  2lgslem1c  27437  2lgslem3  27448  2lgs  27451  dchrvmasum2if  27541  dchrvmasumiflem1  27545  rpvmasum2  27556  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  padicabv  27674  ostth2lem4  27680  nosupno  27748  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfbnd1  27774  maxs1  27810  maxs2  27811  mins1  27812  mins2  27813  abssid  28265  abssge0  28269  axlowdimlem15  28971  opvtxval  29020  opiedgval  29023  elimifd  32556  elim2if  32557  ifeq3da  32559  ifnefals  32561  fmptunsnop  32709  indval2  32839  ind1  32842  pmtridf1o  33114  fzto1stfv1  33121  resvid2  33354  2sqr3minply  33791  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  sigaclfu2  34122  ddeval1  34235  eulerpartlemb  34370  ballotlemsima  34518  ballotlemrv1  34523  signsw0glem  34568  signswmnd  34572  signswrid  34573  indispconn  35239  ex-sategoelel  35426  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  mrsubvr  35516  dfrdg2  35796  dfrdg3  35797  unisnif  35926  dfrdg4  35952  fnejoin2  36370  unbdqndv2lem2  36511  bj-xpima2sn  36959  finxpreclem1  37390  finxpreclem3  37394  matunitlindflem1  37623  poimirlem2  37629  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  mblfinlem2  37665  mbfposadd  37674  itg2addnclem  37678  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem1  37685  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  itggt0cn  37697  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirclem5  37719  areacirc  37720  fdc  37752  heiborlem4  37821  ac6s6  38179  cdleme27a  40369  cdleme31sn1  40383  cdleme31fv1  40393  cdlemk40t  40920  dihvalb  41239  sticksstones12a  42158  metakunt5  42210  metakunt6  42211  metakunt10  42215  metakunt11  42216  metakunt20  42225  brif2  42263  brif12  42264  evlsbagval  42576  selvvvval  42595  fsuppind  42600  dffltz  42644  pw2f1ocnv  43049  aomclem5  43070  kelac1  43075  arearect  43227  areaquad  43228  oe0rif  43298  cantnfresb  43337  safesnsupfidom1o  43430  safesnsupfilb  43431  clsk1indlem1  44058  refsum2cnlem1  45042  upbdrech2  45320  lptioo2  45646  lptioo1  45647  limsupmnfuzlem  45741  limsupre3uzlem  45750  limsup10exlem  45787  coskpi2  45881  cosknegpi  45884  cncfiooicclem1  45908  cncfiooiccre  45910  dvnxpaek  45957  dvnprodlem1  45961  dvnprodlem3  45963  itgioocnicc  45992  iblcncfioo  45993  volico  45998  sublevolico  45999  volioore  46005  voliooico  46007  voliccico  46014  dirkerper  46111  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem10  46132  fourierdlem32  46154  fourierdlem33  46155  fourierdlem37  46159  fourierdlem62  46183  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem93  46214  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem4  46253  etransclem15  46264  etransclem19  46268  etransclem20  46269  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem27  46276  etransclem31  46280  etransclem32  46281  ioorrnopnxrlem  46321  nnfoctbdjlem  46470  isomenndlem  46545  ovn0val  46565  hoidmv0val  46598  hsphoidmvle2  46600  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  hspdifhsp  46631  hoidifhspdmvle  46635  hspmbllem1  46641  hspmbllem2  46642  hspmbl  46644  volico2  46656  ovnsubadd2lem  46660  ovolval4lem2  46665  ovolval5lem1  46667  afvfundmfveq  47150  dfatafv2iota  47222  dfatafv2eqfv  47273  prproropf1olem3  47492  prproropf1olem4  47493  linc1  48342  lincext3  48373  lindslinindsimp1  48374  el0ldep  48383  islindeps2  48400  itcoval0  48583  ackval0  48601