Theorem iftrue 4493

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  ifcif 4487

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is used by:  iftruei  4494  iftrued  4495  iftrueb  4500  ifsb  4501  ifbi  4510  ifeq2da  4520  ifeq12da  4521  ifclda  4523  ifeqda  4524  elimif  4525  ifbothda  4526  ifid  4528  ifeqor  4539  ifnot  4540  ifan  4541  ifor  4542  2if2  4543  dedth  4546  elimhyp  4553  elimhyp2v  4554  elimhyp3v  4555  elimhyp4v  4556  elimdhyp  4558  keephyp2v  4560  keephyp3v  4561  dfopif  4835  dfopg  4836  somin1  6133  somincom  6134  xpima1  6181  elimdelov  7506  brif1  7507  ovif12  7510  ifmpt2v  7512  tz7.44-1  8389  rdg0n  8417  resixpfo  8930  boxriin  8934  boxcutc  8935  pw2f1olem  9065  unxpdomlem2  9213  unxpdomlem3  9214  infsupprpr  9462  ordtypelem1  9476  wemaplem2  9505  unwdomg  9542  ixpiunwdom  9548  cantnfp1lem2  9644  cantnfp1lem3  9645  ssttrcl  9680  ttrclselem2  9691  acndom  10040  dfac12lem2  10133  fin23lem14  10321  axcc2lem  10424  pwfseqlem2  10648  indval2  12227  ind1  12231  uzin  12902  xrmax1  13205  xrmax2  13206  xrmin1  13207  xrmin2  13208  max1ALT  13216  max0sub  13226  ifle  13227  xmulneg1  13299  fzprval  13618  fztpval  13619  modifeq2int  13974  seqf1olem1  14082  seqf1olem2  14083  bcval2  14346  tpf1ofv0  14538  tpf1ofv1  14539  ccatval1  14619  ccatalpha  14636  swrdccat  14777  pfxccat3a  14780  swrdccat3b  14782  repswswrd  14826  cshword  14833  0csh0  14835  ccatco  14877  sgnn  15136  max0add  15366  absmax  15386  sumrblem  15767  fsumcvg  15768  summolem2a  15771  isum  15775  sumss  15780  sumss2  15782  fsumcvg2  15783  fsumser  15786  fsumsplit  15797  sumsplit  15824  prodrblem  15988  fprodcvg  15989  prodmolem2a  15993  zprod  15996  iprod  15997  iprodn0  15999  prodss  16006  fprodsplit  16025  ruclem2  16292  ruclem3  16293  flodddiv4  16477  sadadd2lem2  16512  sadcf  16515  sadc0  16516  sadcp1  16517  sadcaddlem  16519  smupf  16540  smup0  16541  gcd0val  16559  dfgcd2  16608  eucalgf  16645  eucalginv  16646  eucalglt  16647  lcmf0val  16684  phisum  16854  pc0  16918  pcgcd  16942  pcmptcl  16955  pcmpt  16956  pcmpt2  16957  pcprod  16959  fldivp1  16961  prmreclem2  16981  prmreclem4  16983  1arithlem4  16990  vdwlem6  17050  ramtcl2  17075  ramcl2  17080  ramub1lem1  17090  prmop1  17102  fvprmselelfz  17108  fvprmselgcd1  17109  ressid2  17298  xpsfrnel  17620  xpsaddlem  17631  xpsvsca  17635  mreexexd  17708  gsumval1  18745  mgm2nsgrplem2  18985  sgrp2nmndlem2  18990  symgextfve  19493  symgfixfolem1  19512  pmtrmvd  19530  pmtrfinv  19535  pmtrprfval  19561  pmtrprfvalrn  19562  frgpuptinv  19845  frgpup2  19850  frgpup3lem  19851  cyggex  19972  gsumzsplit  20001  gsummpt1n0  20039  dprdfid  20093  dmdprdsplitlem  20113  sdrgacs  20913  abvtrivd  20944  znf1o  21710  uvcvv1  21948  psrlidm  22120  psrridm  22121  mvrf1  22144  mplmonmul  22196  mplcoe1  22197  mplcoe3  22198  mplcoe5  22200  mplmon2  22221  subrgasclcl  22227  evlslem3  22240  evlslem1  22242  selvvvval  22302  psdmul  22338  psdmvr  22341  coe1tmfv1  22444  ply1sclid  22458  dmatmul  22663  scmatscmiddistr  22674  1mavmul  22714  mulmarep1gsum2  22740  1marepvmarrepid  22741  mdetdiag  22765  mdetralt2  22775  mdetunilem2  22779  mdetunilem7  22784  mdetunilem8  22785  mdetunilem9  22786  mndifsplit  22802  maducoeval2  22806  madugsum  22809  madurid  22810  gsummatr01lem3  22823  gsummatr01  22825  smadiadetglem2  22838  1elcpmat  22881  decpmatid  22936  chfacfscmulgsum  23026  chfacfpmmulgsum  23030  ptpjpre1  23737  ptbasfi  23747  ptpjopn  23778  isfcls  24175  ptcmplem2  24219  ptcmplem3  24220  tsmssplit  24318  dscmet  24738  dscopn  24739  icccmplem2  24990  iccpnfcnv  25112  xrhmeo  25114  pcopt  25190  pcopt2  25191  pcoass  25192  pcorevlem  25194  cmetcaulem  25456  ovolicc1  25684  ioorcl  25745  i1f1lem  25857  itg11  25859  itg1addlem2  25865  itg1addlem4  25867  i1fres  25873  itg1climres  25882  mbfi1fseqlem4  25886  mbfi1fseqlem5  25887  mbfi1flim  25891  itg2const2  25909  itg2seq  25910  itg2uba  25911  itg2splitlem  25916  itg2split  25917  itg2monolem1  25918  itg2cnlem1  25929  itg2cnlem2  25930  iblcnlem  25957  iblss  25973  iblss2  25974  itgitg2  25975  itgle  25978  itgss  25980  itgss2  25981  itgss3  25983  itgless  25985  ibladdlem  25988  itgaddlem1  25991  iblabslem  25996  iblabs  25997  iblabsr  25998  iblmulc2  25999  bddmulibl  26007  bddiblnc  26010  itggt0  26012  itgcn  26013  limcvallem  26039  ellimc2  26045  limccnp  26059  limccnp2  26060  limcco  26061  dvcobr  26114  dvexp2  26122  mon1pid  26320  elply2  26362  elplyd  26368  ply1termlem  26369  coe1termlem  26424  abelthlem9  26612  logtayl  26834  leibpilem2  27115  leibpi  27116  rlimcnp2  27140  efrlim  27143  igamz  27221  isnsqf  27308  mule1  27321  sqff1o  27355  muinv  27366  chtublem  27384  dchrelbasd  27412  bposlem1  27457  bposlem3  27459  bposlem5  27461  bposlem6  27462  lgsval2lem  27480  lgsneg  27494  lgsdilem  27497  lgsdir2  27503  lgsdir  27505  lgsdi  27507  lgsne0  27508  gausslemma2dlem1a  27538  2lgslem1c  27566  2lgslem3  27577  2lgs  27580  dchrvmasum2if  27670  dchrvmasumiflem1  27674  rpvmasum2  27685  pntrlog2bndlem4  27753  pntrlog2bndlem5  27754  padicabv  27803  ostth2lem4  27809  nosupno  27876  nosupbday  27878  nosupbnd1  27887  nosupbnd2  27889  noinfno  27891  noinfbday  27893  noinfbnd1  27902  maxs1  27942  maxs2  27943  mins1  27944  mins2  27945  abssid  28443  abssge0  28447  axlowdimlem15  29315  opvtxval  29362  opiedgval  29365  elimifd  32898  elim2if  32899  ifeq3da  32901  ifnefals  32903  fmptunsnop  33054  pmtridf1o  33423  fzto1stfv1  33430  resvid2  33659  psrmonmul  33949  vieta  33979  2sqr3minply  34179  cos9thpiminply  34187  xrge0iifcnv  34332  xrge0iifiso  34334  xrge0iifhom  34336  sigaclfu2  34520  ddeval1  34633  eulerpartlemb  34767  ballotlemsima  34915  ballotlemrv1  34920  signsw0glem  34949  signswmnd  34953  signswrid  34954  vonf1oonfo  35607  indispconn  35734  ex-sategoelel  35921  ex-sategoelelomsuc  35926  ex-sategoelel12  35927  mrsubvr  36011  dfrdg2  36293  dfrdg3  36294  unisnif  36423  dfrdg4  36451  fnejoin2  36908  unbdqndv2lem2  37127  bj-xpima2sn  37622  finxpreclem1  38063  finxpreclem3  38067  matunitlindflem1  38295  poimirlem2  38301  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem24  38323  mblfinlem2  38337  mbfposadd  38346  itg2addnclem  38350  itg2gt0cn  38354  ibladdnclem  38355  itgaddnclem1  38357  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  itggt0cn  38369  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  areacirclem5  38391  areacirc  38392  fdc  38424  heiborlem4  38493  ac6s6  38849  cdleme27a  41169  cdleme31sn1  41183  cdleme31fv1  41193  cdlemk40t  41720  dihvalb  42039  sticksstones12a  42952  brif2  43023  brif12  43024  evlsbagval  43346  fsuppind  43350  dffltz  43394  pw2f1ocnv  43792  aomclem5  43813  kelac1  43818  arearect  43970  areaquad  43971  oe0rif  44040  cantnfresb  44079  safesnsupfidom1o  44171  safesnsupfilb  44172  clsk1indlem1  44799  refsum2cnlem1  45785  upbdrech2  46055  lptioo2  46375  lptioo1  46376  limsupmnfuzlem  46468  limsupre3uzlem  46477  limsup10exlem  46514  coskpi2  46608  cosknegpi  46611  cncfiooicclem1  46635  cncfiooiccre  46637  dvnxpaek  46684  dvnprodlem1  46688  dvnprodlem3  46690  itgioocnicc  46719  iblcncfioo  46720  volico  46725  sublevolico  46726  volioore  46732  voliooico  46734  voliccico  46741  dirkerper  46838  dirkertrigeq  46843  dirkercncflem2  46846  fourierdlem10  46859  fourierdlem32  46881  fourierdlem33  46882  fourierdlem37  46886  fourierdlem62  46910  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem79  46927  fourierdlem81  46929  fourierdlem82  46930  fourierdlem93  46941  fourierdlem97  46945  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  etransclem4  46980  etransclem15  46991  etransclem19  46995  etransclem20  46996  etransclem23  46999  etransclem24  47000  etransclem25  47001  etransclem27  47003  etransclem31  47007  etransclem32  47008  ioorrnopnxrlem  47048  nnfoctbdjlem  47197  isomenndlem  47272  ovn0val  47292  hoidmv0val  47325  hsphoidmvle2  47327  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmv1le  47336  hoidmvlelem2  47338  hoidmvlelem3  47339  ovnhoilem1  47343  hspdifhsp  47358  hoidifhspdmvle  47362  hspmbllem1  47368  hspmbllem2  47369  hspmbl  47371  volico2  47383  ovnsubadd2lem  47387  ovolval4lem2  47392  ovolval5lem1  47394  afvfundmfveq  47903  dfatafv2iota  47975  dfatafv2eqfv  48026  difmodm1lt  48130  prproropf1olem3  48282  prproropf1olem4  48283  linc1  49233  lincext3  49264  lindslinindsimp1  49265  el0ldep  49274  islindeps2  49291  itcoval0  49470  ackval0  49488  crosspv1i  50669  crosspv2i  50670