Theorem iftrue 4426

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 4422	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1039	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	abbi2dv 2889	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2812	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2735  ifcif 4420

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-if 4421

This theorem is referenced by:  iftruei  4427  iftrued  4428  ifsb  4433  ifbi  4442  ifeq2da  4452  ifeq12da  4453  ifclda  4455  ifeqda  4456  elimif  4457  ifbothda  4458  ifid  4460  ifeqor  4471  ifnot  4472  ifan  4473  ifor  4474  2if2  4475  dedth  4478  elimhyp  4485  elimhyp2v  4486  elimhyp3v  4487  elimhyp4v  4488  elimdhyp  4490  keephyp2v  4492  keephyp3v  4493  dfopifOLD  4758  dfopg  4759  somin1  5965  somincom  5966  xpima1  6012  elimdelov  7244  ovif12  7247  tz7.44-1  8052  resixpfo  8518  boxriin  8522  boxcutc  8523  pw2f1olem  8642  unxpdomlem2  8761  unxpdomlem3  8762  infsupprpr  9001  ordtypelem1  9015  wemaplem2  9044  unwdomg  9081  ixpiunwdom  9087  cantnfp1lem2  9175  cantnfp1lem3  9176  acndom  9511  dfac12lem2  9604  fin23lem14  9793  axcc2lem  9896  pwfseqlem2  10119  uzin  12318  xrmax1  12609  xrmax2  12610  xrmin1  12611  xrmin2  12612  max1ALT  12620  max0sub  12630  ifle  12631  xmulneg1  12703  fzprval  13017  fztpval  13018  modifeq2int  13350  seqf1olem1  13459  seqf1olem2  13460  bcval2  13715  ccatval1  13977  ccatval1OLD  13978  ccatalpha  13994  swrdccat  14144  pfxccat3a  14147  swrdccat3b  14149  repswswrd  14193  cshword  14200  0csh0  14202  ccatco  14244  sgnn  14501  max0add  14718  absmax  14737  sumrblem  15116  fsumcvg  15117  summolem2a  15120  isum  15124  sumss  15129  sumss2  15131  fsumcvg2  15132  fsumser  15135  fsumsplit  15145  sumsplit  15171  prodrblem  15331  fprodcvg  15332  prodmolem2a  15336  zprod  15339  iprod  15340  iprodn0  15342  prodss  15349  fprodsplit  15368  ruclem2  15633  ruclem3  15634  flodddiv4  15814  sadadd2lem2  15849  sadcf  15852  sadc0  15853  sadcp1  15854  sadcaddlem  15856  smupf  15877  smup0  15878  gcd0val  15896  dfgcd2  15945  eucalgf  15979  eucalginv  15980  eucalglt  15981  lcmf0val  16018  phisum  16182  pc0  16246  pcgcd  16269  pcmptcl  16282  pcmpt  16283  pcmpt2  16284  pcprod  16286  fldivp1  16288  prmreclem2  16308  prmreclem4  16310  1arithlem4  16317  vdwlem6  16377  ramtcl2  16402  ramcl2  16407  ramub1lem1  16417  prmop1  16429  fvprmselelfz  16435  fvprmselgcd1  16436  ressid2  16610  xpsfrnel  16893  xpsaddlem  16904  xpsvsca  16908  mreexexd  16977  gsumval1  17959  mgm2nsgrplem2  18150  sgrp2nmndlem2  18155  symgextfve  18614  symgfixfolem1  18633  pmtrmvd  18651  pmtrfinv  18656  pmtrprfval  18682  pmtrprfvalrn  18683  frgpuptinv  18964  frgpup2  18969  frgpup3lem  18970  cyggex  19086  gsumzsplit  19115  gsummpt1n0  19153  dprdfid  19207  dmdprdsplitlem  19227  sdrgacs  19648  abvtrivd  19679  znf1o  20319  uvcvv1  20554  psrlidm  20731  psrridm  20732  mvrf1  20753  mplmonmul  20796  mplcoe1  20797  mplcoe3  20798  mplcoe5  20800  mplmon2  20822  subrgasclcl  20828  evlslem3  20843  evlslem1  20845  coe1tmfv1  20998  ply1sclid  21012  dmatmul  21197  scmatscmiddistr  21208  1mavmul  21248  mulmarep1gsum2  21274  1marepvmarrepid  21275  mdetdiag  21299  mdetralt2  21309  mdetunilem2  21313  mdetunilem7  21318  mdetunilem8  21319  mdetunilem9  21320  mndifsplit  21336  maducoeval2  21340  madugsum  21343  madurid  21344  gsummatr01lem3  21357  gsummatr01  21359  smadiadetglem2  21372  1elcpmat  21415  decpmatid  21470  chfacfscmulgsum  21560  chfacfpmmulgsum  21564  ptpjpre1  22271  ptbasfi  22281  ptpjopn  22312  isfcls  22709  ptcmplem2  22753  ptcmplem3  22754  tsmssplit  22852  dscmet  23274  dscopn  23275  icccmplem2  23524  iccpnfcnv  23645  xrhmeo  23647  pcopt  23723  pcopt2  23724  pcoass  23725  pcorevlem  23727  cmetcaulem  23988  ovolicc1  24216  ioorcl  24277  i1f1lem  24389  itg11  24391  itg1addlem2  24397  itg1addlem4  24399  i1fres  24405  itg1climres  24414  mbfi1fseqlem4  24418  mbfi1fseqlem5  24419  mbfi1flim  24423  itg2const2  24441  itg2seq  24442  itg2uba  24443  itg2splitlem  24448  itg2split  24449  itg2monolem1  24450  itg2cnlem1  24461  itg2cnlem2  24462  iblcnlem  24488  iblss  24504  iblss2  24505  itgitg2  24506  itgle  24509  itgss  24511  itgss2  24512  itgss3  24514  itgless  24516  ibladdlem  24519  itgaddlem1  24522  iblabslem  24527  iblabs  24528  iblabsr  24529  iblmulc2  24530  bddmulibl  24538  bddiblnc  24541  itggt0  24543  itgcn  24544  limcvallem  24570  ellimc2  24576  limccnp  24590  limccnp2  24591  limcco  24592  dvcobr  24645  dvexp2  24653  elply2  24892  elplyd  24898  ply1termlem  24899  coe1termlem  24954  abelthlem9  25134  logtayl  25350  leibpilem2  25626  leibpi  25627  rlimcnp2  25651  efrlim  25654  igamz  25732  isnsqf  25819  mule1  25832  sqff1o  25866  muinv  25877  chtublem  25894  dchrelbasd  25922  bposlem1  25967  bposlem3  25969  bposlem5  25971  bposlem6  25972  lgsval2lem  25990  lgsneg  26004  lgsdilem  26007  lgsdir2  26013  lgsdir  26015  lgsdi  26017  lgsne0  26018  gausslemma2dlem1a  26048  2lgslem1c  26076  2lgslem3  26087  2lgs  26090  dchrvmasum2if  26180  dchrvmasumiflem1  26184  rpvmasum2  26195  pntrlog2bndlem4  26263  pntrlog2bndlem5  26264  padicabv  26313  ostth2lem4  26319  axlowdimlem15  26849  opvtxval  26895  opiedgval  26898  elimifd  30408  elim2if  30409  ifeq3da  30411  pmtridf1o  30887  fzto1stfv1  30894  resvid2  31053  xrge0iifcnv  31404  xrge0iifiso  31406  xrge0iifhom  31408  indval2  31501  ind1  31504  sigaclfu2  31608  ddeval1  31721  eulerpartlemb  31854  ballotlemsima  32001  ballotlemrv1  32006  signsw0glem  32051  signswmnd  32055  signswrid  32056  indispconn  32712  ex-sategoelel  32899  ex-sategoelelomsuc  32904  ex-sategoelel12  32905  mrsubvr  32989  dfrdg2  33287  dfrdg3  33288  nosupno  33471  nosupbday  33473  nosupbnd1  33482  nosupbnd2  33484  noinfno  33486  noinfbday  33488  noinfbnd1  33497  unisnif  33776  dfrdg4  33802  fnejoin2  34107  unbdqndv2lem2  34239  bj-xpima2sn  34675  finxpreclem1  35086  finxpreclem3  35090  matunitlindflem1  35333  poimirlem2  35339  poimirlem15  35352  poimirlem16  35353  poimirlem17  35354  poimirlem19  35356  poimirlem20  35357  poimirlem24  35361  mblfinlem2  35375  mbfposadd  35384  itg2addnclem  35388  itg2gt0cn  35392  ibladdnclem  35393  itgaddnclem1  35395  iblabsnclem  35400  iblabsnc  35401  iblmulc2nc  35402  itggt0cn  35407  ftc1anclem4  35413  ftc1anclem5  35414  ftc1anclem6  35415  ftc1anclem7  35416  ftc1anclem8  35417  ftc1anc  35418  areacirclem5  35429  areacirc  35430  fdc  35463  heiborlem4  35532  ac6s6  35890  cdleme27a  37943  cdleme31sn1  37957  cdleme31fv1  37967  cdlemk40t  38494  dihvalb  38813  metakunt5  39651  metakunt6  39652  metakunt10  39656  metakunt11  39657  metakunt20  39666  brif1  39703  brif2  39704  brif12  39705  evlsbagval  39780  fsuppind  39784  dffltz  39963  pw2f1ocnv  40351  aomclem5  40375  kelac1  40380  mon1pid  40522  arearect  40538  areaquad  40539  clsk1indlem1  41121  refsum2cnlem1  42039  upbdrech2  42308  lptioo2  42639  lptioo1  42640  limsupmnfuzlem  42734  limsupre3uzlem  42743  limsup10exlem  42780  coskpi2  42874  cosknegpi  42877  cncfiooicclem1  42901  cncfiooiccre  42903  dvnxpaek  42950  dvnprodlem1  42954  dvnprodlem3  42956  itgioocnicc  42985  iblcncfioo  42986  volico  42991  sublevolico  42992  volioore  42998  voliooico  43000  voliccico  43007  dirkerper  43104  dirkertrigeq  43109  dirkercncflem2  43112  fourierdlem10  43125  fourierdlem32  43147  fourierdlem33  43148  fourierdlem37  43152  fourierdlem62  43176  fourierdlem73  43187  fourierdlem74  43188  fourierdlem75  43189  fourierdlem79  43193  fourierdlem81  43195  fourierdlem82  43196  fourierdlem93  43207  fourierdlem97  43211  fourierdlem101  43215  fourierdlem103  43217  fourierdlem104  43218  sqwvfoura  43236  sqwvfourb  43237  fourierswlem  43238  fouriersw  43239  etransclem4  43246  etransclem15  43257  etransclem19  43261  etransclem20  43262  etransclem23  43265  etransclem24  43266  etransclem25  43267  etransclem27  43269  etransclem31  43273  etransclem32  43274  ioorrnopnxrlem  43314  nnfoctbdjlem  43460  isomenndlem  43535  ovn0val  43555  hoidmv0val  43588  hsphoidmvle2  43590  hoidmv1lelem1  43596  hoidmv1lelem2  43597  hoidmv1le  43599  hoidmvlelem2  43601  hoidmvlelem3  43602  ovnhoilem1  43606  hspdifhsp  43621  hoidifhspdmvle  43625  hspmbllem1  43631  hspmbllem2  43632  hspmbl  43634  volico2  43646  ovnsubadd2lem  43650  ovolval4lem2  43655  ovolval5lem1  43657  afvfundmfveq  44062  dfatafv2iota  44134  dfatafv2eqfv  44185  prproropf1olem3  44390  prproropf1olem4  44391  linc1  45199  lincext3  45230  lindslinindsimp1  45231  el0ldep  45240  islindeps2  45257  itcoval0  45441  ackval0  45459