Theorem iftrue 4482

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2711  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  iftruei  4483  iftrued  4484  iftrueb  4489  ifsb  4490  ifbi  4499  ifeq2da  4509  ifeq12da  4510  ifclda  4512  ifeqda  4513  elimif  4514  ifbothda  4515  ifid  4517  ifeqor  4528  ifnot  4529  ifan  4530  ifor  4531  2if2  4532  dedth  4535  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elimdhyp  4547  keephyp2v  4549  keephyp3v  4550  dfopif  4823  dfopg  4824  somin1  6087  somincom  6088  xpima1  6138  elimdelov  7451  brif1  7452  ovif12  7455  ifmpt2v  7457  tz7.44-1  8334  rdg0n  8362  resixpfo  8869  boxriin  8873  boxcutc  8874  pw2f1olem  9004  unxpdomlem2  9151  unxpdomlem3  9152  infsupprpr  9400  ordtypelem1  9414  wemaplem2  9443  unwdomg  9480  ixpiunwdom  9486  cantnfp1lem2  9579  cantnfp1lem3  9580  ssttrcl  9615  ttrclselem2  9626  acndom  9952  dfac12lem2  10046  fin23lem14  10234  axcc2lem  10337  pwfseqlem2  10560  uzin  12782  xrmax1  13084  xrmax2  13085  xrmin1  13086  xrmin2  13087  max1ALT  13095  max0sub  13105  ifle  13106  xmulneg1  13178  fzprval  13495  fztpval  13496  modifeq2int  13850  seqf1olem1  13958  seqf1olem2  13959  bcval2  14222  tpf1ofv0  14413  tpf1ofv1  14414  ccatval1  14494  ccatalpha  14511  swrdccat  14652  pfxccat3a  14655  swrdccat3b  14657  repswswrd  14701  cshword  14708  0csh0  14710  ccatco  14752  sgnn  15011  max0add  15227  absmax  15247  sumrblem  15628  fsumcvg  15629  summolem2a  15632  isum  15636  sumss  15641  sumss2  15643  fsumcvg2  15644  fsumser  15647  fsumsplit  15658  sumsplit  15685  prodrblem  15846  fprodcvg  15847  prodmolem2a  15851  zprod  15854  iprod  15855  iprodn0  15857  prodss  15864  fprodsplit  15883  ruclem2  16151  ruclem3  16152  flodddiv4  16336  sadadd2lem2  16371  sadcf  16374  sadc0  16375  sadcp1  16376  sadcaddlem  16378  smupf  16399  smup0  16400  gcd0val  16418  dfgcd2  16467  eucalgf  16504  eucalginv  16505  eucalglt  16506  lcmf0val  16543  phisum  16712  pc0  16776  pcgcd  16800  pcmptcl  16813  pcmpt  16814  pcmpt2  16815  pcprod  16817  fldivp1  16819  prmreclem2  16839  prmreclem4  16841  1arithlem4  16848  vdwlem6  16908  ramtcl2  16933  ramcl2  16938  ramub1lem1  16948  prmop1  16960  fvprmselelfz  16966  fvprmselgcd1  16967  ressid2  17155  xpsfrnel  17476  xpsaddlem  17487  xpsvsca  17491  mreexexd  17564  gsumval1  18601  mgm2nsgrplem2  18837  sgrp2nmndlem2  18842  symgextfve  19341  symgfixfolem1  19360  pmtrmvd  19378  pmtrfinv  19383  pmtrprfval  19409  pmtrprfvalrn  19410  frgpuptinv  19693  frgpup2  19698  frgpup3lem  19699  cyggex  19820  gsumzsplit  19849  gsummpt1n0  19887  dprdfid  19941  dmdprdsplitlem  19961  sdrgacs  20726  abvtrivd  20757  znf1o  21498  uvcvv1  21736  psrlidm  21909  psrridm  21910  mvrf1  21933  mplmonmul  21981  mplcoe1  21982  mplcoe3  21983  mplcoe5  21985  mplmon2  22006  subrgasclcl  22012  evlslem3  22025  evlslem1  22027  psdmul  22091  psdmvr  22094  coe1tmfv1  22198  ply1sclid  22212  dmatmul  22422  scmatscmiddistr  22433  1mavmul  22473  mulmarep1gsum2  22499  1marepvmarrepid  22500  mdetdiag  22524  mdetralt2  22534  mdetunilem2  22538  mdetunilem7  22543  mdetunilem8  22544  mdetunilem9  22545  mndifsplit  22561  maducoeval2  22565  madugsum  22568  madurid  22569  gsummatr01lem3  22582  gsummatr01  22584  smadiadetglem2  22597  1elcpmat  22640  decpmatid  22695  chfacfscmulgsum  22785  chfacfpmmulgsum  22789  ptpjpre1  23496  ptbasfi  23506  ptpjopn  23537  isfcls  23934  ptcmplem2  23978  ptcmplem3  23979  tsmssplit  24077  dscmet  24497  dscopn  24498  icccmplem2  24749  iccpnfcnv  24879  xrhmeo  24881  pcopt  24959  pcopt2  24960  pcoass  24961  pcorevlem  24963  cmetcaulem  25225  ovolicc1  25454  ioorcl  25515  i1f1lem  25627  itg11  25629  itg1addlem2  25635  itg1addlem4  25637  i1fres  25643  itg1climres  25652  mbfi1fseqlem4  25656  mbfi1fseqlem5  25657  mbfi1flim  25661  itg2const2  25679  itg2seq  25680  itg2uba  25681  itg2splitlem  25686  itg2split  25687  itg2monolem1  25688  itg2cnlem1  25699  itg2cnlem2  25700  iblcnlem  25727  iblss  25743  iblss2  25744  itgitg2  25745  itgle  25748  itgss  25750  itgss2  25751  itgss3  25753  itgless  25755  ibladdlem  25758  itgaddlem1  25761  iblabslem  25766  iblabs  25767  iblabsr  25768  iblmulc2  25769  bddmulibl  25777  bddiblnc  25780  itggt0  25782  itgcn  25783  limcvallem  25809  ellimc2  25815  limccnp  25829  limccnp2  25830  limcco  25831  dvcobr  25886  dvcobrOLD  25887  dvexp2  25895  mon1pid  26096  elply2  26138  elplyd  26144  ply1termlem  26145  coe1termlem  26200  abelthlem9  26387  logtayl  26606  leibpilem2  26888  leibpi  26889  rlimcnp2  26913  efrlim  26916  efrlimOLD  26917  igamz  26995  isnsqf  27082  mule1  27095  sqff1o  27129  muinv  27140  chtublem  27159  dchrelbasd  27187  bposlem1  27232  bposlem3  27234  bposlem5  27236  bposlem6  27237  lgsval2lem  27255  lgsneg  27269  lgsdilem  27272  lgsdir2  27278  lgsdir  27280  lgsdi  27282  lgsne0  27283  gausslemma2dlem1a  27313  2lgslem1c  27341  2lgslem3  27352  2lgs  27355  dchrvmasum2if  27445  dchrvmasumiflem1  27449  rpvmasum2  27460  pntrlog2bndlem4  27528  pntrlog2bndlem5  27529  padicabv  27578  ostth2lem4  27584  nosupno  27652  nosupbday  27654  nosupbnd1  27663  nosupbnd2  27665  noinfno  27667  noinfbday  27669  noinfbnd1  27678  maxs1  27714  maxs2  27715  mins1  27716  mins2  27717  abssid  28189  abssge0  28193  axlowdimlem15  28945  opvtxval  28992  opiedgval  28995  elimifd  32534  elim2if  32535  ifeq3da  32537  ifnefals  32539  fmptunsnop  32692  indval2  32846  ind1  32849  pmtridf1o  33074  fzto1stfv1  33081  resvid2  33306  2sqr3minply  33804  cos9thpiminply  33812  xrge0iifcnv  33957  xrge0iifiso  33959  xrge0iifhom  33961  sigaclfu2  34145  ddeval1  34258  eulerpartlemb  34392  ballotlemsima  34540  ballotlemrv1  34545  signsw0glem  34577  signswmnd  34581  signswrid  34582  indispconn  35289  ex-sategoelel  35476  ex-sategoelelomsuc  35481  ex-sategoelel12  35482  mrsubvr  35566  dfrdg2  35848  dfrdg3  35849  unisnif  35978  dfrdg4  36006  fnejoin2  36424  unbdqndv2lem2  36565  bj-xpima2sn  37013  finxpreclem1  37444  finxpreclem3  37448  matunitlindflem1  37666  poimirlem2  37672  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem24  37694  mblfinlem2  37708  mbfposadd  37717  itg2addnclem  37721  itg2gt0cn  37725  ibladdnclem  37726  itgaddnclem1  37728  iblabsnclem  37733  iblabsnc  37734  iblmulc2nc  37735  itggt0cn  37740  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  areacirclem5  37762  areacirc  37763  fdc  37795  heiborlem4  37864  ac6s6  38222  cdleme27a  40476  cdleme31sn1  40490  cdleme31fv1  40500  cdlemk40t  41027  dihvalb  41346  sticksstones12a  42260  brif2  42332  brif12  42333  evlsbagval  42674  selvvvval  42693  fsuppind  42698  dffltz  42742  pw2f1ocnv  43144  aomclem5  43165  kelac1  43170  arearect  43322  areaquad  43323  oe0rif  43392  cantnfresb  43431  safesnsupfidom1o  43524  safesnsupfilb  43525  clsk1indlem1  44152  refsum2cnlem1  45148  upbdrech2  45423  lptioo2  45745  lptioo1  45746  limsupmnfuzlem  45838  limsupre3uzlem  45847  limsup10exlem  45884  coskpi2  45978  cosknegpi  45981  cncfiooicclem1  46005  cncfiooiccre  46007  dvnxpaek  46054  dvnprodlem1  46058  dvnprodlem3  46060  itgioocnicc  46089  iblcncfioo  46090  volico  46095  sublevolico  46096  volioore  46102  voliooico  46104  voliccico  46111  dirkerper  46208  dirkertrigeq  46213  dirkercncflem2  46216  fourierdlem10  46229  fourierdlem32  46251  fourierdlem33  46252  fourierdlem37  46256  fourierdlem62  46280  fourierdlem73  46291  fourierdlem74  46292  fourierdlem75  46293  fourierdlem79  46297  fourierdlem81  46299  fourierdlem82  46300  fourierdlem93  46311  fourierdlem97  46315  fourierdlem101  46319  fourierdlem103  46321  fourierdlem104  46322  sqwvfoura  46340  sqwvfourb  46341  fourierswlem  46342  fouriersw  46343  etransclem4  46350  etransclem15  46361  etransclem19  46365  etransclem20  46366  etransclem23  46369  etransclem24  46370  etransclem25  46371  etransclem27  46373  etransclem31  46377  etransclem32  46378  ioorrnopnxrlem  46418  nnfoctbdjlem  46567  isomenndlem  46642  ovn0val  46662  hoidmv0val  46695  hsphoidmvle2  46697  hoidmv1lelem1  46703  hoidmv1lelem2  46704  hoidmv1le  46706  hoidmvlelem2  46708  hoidmvlelem3  46709  ovnhoilem1  46713  hspdifhsp  46728  hoidifhspdmvle  46732  hspmbllem1  46738  hspmbllem2  46739  hspmbl  46741  volico2  46753  ovnsubadd2lem  46757  ovolval4lem2  46762  ovolval5lem1  46764  afvfundmfveq  47252  dfatafv2iota  47324  dfatafv2eqfv  47375  difmodm1lt  47473  prproropf1olem3  47619  prproropf1olem4  47620  linc1  48540  lincext3  48571  lindslinindsimp1  48572  el0ldep  48581  islindeps2  48598  itcoval0  48777  ackval0  48795