Theorem iftrue 4480

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554   ∈ wcel 2136  {cab 2734  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-if 4475

This theorem is referenced by:  iftruei  4481  iftrued  4482  iftrueb  4487  ifsb  4488  ifbi  4497  ifeq2da  4507  ifeq12da  4508  ifclda  4510  ifeqda  4511  elimif  4512  ifbothda  4513  ifid  4515  ifeqor  4526  ifnot  4527  ifan  4528  ifor  4529  2if2  4530  dedth  4533  elimhyp  4540  elimhyp2v  4541  elimhyp3v  4542  elimhyp4v  4543  elimdhyp  4545  keephyp2v  4547  keephyp3v  4548  dfopif  4822  dfopg  4823  somin1  6110  somincom  6111  xpima1  6158  elimdelov  7481  brif1  7482  ovif12  7485  ifmpt2v  7487  tz7.44-1  8365  rdg0n  8393  resixpfo  8907  boxriin  8911  boxcutc  8912  pw2f1olem  9042  unxpdomlem2  9190  unxpdomlem3  9191  infsupprpr  9442  ordtypelem1  9456  wemaplem2  9485  unwdomg  9522  ixpiunwdom  9528  cantnfp1lem2  9624  cantnfp1lem3  9625  ssttrcl  9660  ttrclselem2  9671  acndom  9997  dfac12lem2  10091  fin23lem14  10280  axcc2lem  10383  pwfseqlem2  10607  indval2  12190  ind1  12194  uzin  12865  xrmax1  13168  xrmax2  13169  xrmin1  13170  xrmin2  13171  max1ALT  13179  max0sub  13189  ifle  13190  xmulneg1  13262  fzprval  13580  fztpval  13581  modifeq2int  13936  seqf1olem1  14044  seqf1olem2  14045  bcval2  14308  tpf1ofv0  14499  tpf1ofv1  14500  ccatval1  14580  ccatalpha  14597  swrdccat  14738  pfxccat3a  14741  swrdccat3b  14743  repswswrd  14787  cshword  14794  0csh0  14796  ccatco  14838  sgnn  15097  max0add  15313  absmax  15333  sumrblem  15714  fsumcvg  15715  summolem2a  15718  isum  15722  sumss  15727  sumss2  15729  fsumcvg2  15730  fsumser  15733  fsumsplit  15744  sumsplit  15771  prodrblem  15935  fprodcvg  15936  prodmolem2a  15940  zprod  15943  iprod  15944  iprodn0  15946  prodss  15953  fprodsplit  15972  ruclem2  16240  ruclem3  16241  flodddiv4  16425  sadadd2lem2  16460  sadcf  16463  sadc0  16464  sadcp1  16465  sadcaddlem  16467  smupf  16488  smup0  16489  gcd0val  16507  dfgcd2  16556  eucalgf  16593  eucalginv  16594  eucalglt  16595  lcmf0val  16632  phisum  16802  pc0  16866  pcgcd  16890  pcmptcl  16903  pcmpt  16904  pcmpt2  16905  pcprod  16907  fldivp1  16909  prmreclem2  16929  prmreclem4  16931  1arithlem4  16938  vdwlem6  16998  ramtcl2  17023  ramcl2  17028  ramub1lem1  17038  prmop1  17050  fvprmselelfz  17056  fvprmselgcd1  17057  ressid2  17246  xpsfrnel  17568  xpsaddlem  17579  xpsvsca  17583  mreexexd  17656  gsumval1  18693  mgm2nsgrplem2  18932  sgrp2nmndlem2  18937  symgextfve  19435  symgfixfolem1  19454  pmtrmvd  19472  pmtrfinv  19477  pmtrprfval  19503  pmtrprfvalrn  19504  frgpuptinv  19787  frgpup2  19792  frgpup3lem  19793  cyggex  19914  gsumzsplit  19943  gsummpt1n0  19981  dprdfid  20035  dmdprdsplitlem  20055  sdrgacs  20823  abvtrivd  20854  znf1o  21576  uvcvv1  21814  psrlidm  21986  psrridm  21987  mvrf1  22010  mplmonmul  22062  mplcoe1  22063  mplcoe3  22064  mplcoe5  22066  mplmon2  22087  subrgasclcl  22093  evlslem3  22106  evlslem1  22108  selvvvval  22168  psdmul  22204  psdmvr  22207  coe1tmfv1  22310  ply1sclid  22324  dmatmul  22530  scmatscmiddistr  22541  1mavmul  22581  mulmarep1gsum2  22607  1marepvmarrepid  22608  mdetdiag  22632  mdetralt2  22642  mdetunilem2  22646  mdetunilem7  22651  mdetunilem8  22652  mdetunilem9  22653  mndifsplit  22669  maducoeval2  22673  madugsum  22676  madurid  22677  gsummatr01lem3  22690  gsummatr01  22692  smadiadetglem2  22705  1elcpmat  22748  decpmatid  22803  chfacfscmulgsum  22893  chfacfpmmulgsum  22897  ptpjpre1  23604  ptbasfi  23614  ptpjopn  23645  isfcls  24042  ptcmplem2  24086  ptcmplem3  24087  tsmssplit  24185  dscmet  24605  dscopn  24606  icccmplem2  24857  iccpnfcnv  24979  xrhmeo  24981  pcopt  25057  pcopt2  25058  pcoass  25059  pcorevlem  25061  cmetcaulem  25323  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  25981  dvexp2  25989  mon1pid  26187  elply2  26229  elplyd  26235  ply1termlem  26236  coe1termlem  26291  abelthlem9  26473  logtayl  26695  leibpilem2  26976  leibpi  26977  rlimcnp2  27001  efrlim  27004  igamz  27082  isnsqf  27169  mule1  27182  sqff1o  27216  muinv  27227  chtublem  27245  dchrelbasd  27273  bposlem1  27318  bposlem3  27320  bposlem5  27322  bposlem6  27323  lgsval2lem  27341  lgsneg  27355  lgsdilem  27358  lgsdir2  27364  lgsdir  27366  lgsdi  27368  lgsne0  27369  gausslemma2dlem1a  27399  2lgslem1c  27427  2lgslem3  27438  2lgs  27441  dchrvmasum2if  27531  dchrvmasumiflem1  27535  rpvmasum2  27546  pntrlog2bndlem4  27614  pntrlog2bndlem5  27615  padicabv  27664  ostth2lem4  27670  nosupno  27737  nosupbday  27739  nosupbnd1  27748  nosupbnd2  27750  noinfno  27752  noinfbday  27754  noinfbnd1  27763  maxs1  27803  maxs2  27804  mins1  27805  mins2  27806  abssid  28304  abssge0  28308  axlowdimlem15  29096  opvtxval  29143  opiedgval  29146  elimifd  32684  elim2if  32685  ifeq3da  32687  ifnefals  32689  fmptunsnop  32845  pmtridf1o  33228  fzto1stfv1  33235  resvid2  33470  psrmonmul  33801  vieta  33831  2sqr3minply  34031  cos9thpiminply  34039  xrge0iifcnv  34184  xrge0iifiso  34186  xrge0iifhom  34188  sigaclfu2  34372  ddeval1  34485  eulerpartlemb  34619  ballotlemsima  34767  ballotlemrv1  34772  signsw0glem  34804  signswmnd  34808  signswrid  34809  indispconn  35532  ex-sategoelel  35719  ex-sategoelelomsuc  35724  ex-sategoelel12  35725  mrsubvr  35809  dfrdg2  36091  dfrdg3  36092  unisnif  36221  dfrdg4  36249  fnejoin2  36677  unbdqndv2lem2  36896  bj-xpima2sn  37391  finxpreclem1  37831  finxpreclem3  37835  matunitlindflem1  38063  poimirlem2  38069  poimirlem15  38082  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem24  38091  mblfinlem2  38105  mbfposadd  38114  itg2addnclem  38118  itg2gt0cn  38122  ibladdnclem  38123  itgaddnclem1  38125  iblabsnclem  38130  iblabsnc  38131  iblmulc2nc  38132  itggt0cn  38137  ftc1anclem4  38143  ftc1anclem5  38144  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  areacirclem5  38159  areacirc  38160  fdc  38192  heiborlem4  38261  ac6s6  38619  cdleme27a  40939  cdleme31sn1  40953  cdleme31fv1  40963  cdlemk40t  41490  dihvalb  41809  sticksstones12a  42722  brif2  42791  brif12  42792  evlsbagval  43116  fsuppind  43120  dffltz  43164  pw2f1ocnv  43562  aomclem5  43583  kelac1  43588  arearect  43740  areaquad  43741  oe0rif  43810  cantnfresb  43849  safesnsupfidom1o  43941  safesnsupfilb  43942  clsk1indlem1  44569  refsum2cnlem1  45565  upbdrech2  45835  lptioo2  46155  lptioo1  46156  limsupmnfuzlem  46248  limsupre3uzlem  46257  limsup10exlem  46294  coskpi2  46388  cosknegpi  46391  cncfiooicclem1  46415  cncfiooiccre  46417  dvnxpaek  46464  dvnprodlem1  46468  dvnprodlem3  46470  itgioocnicc  46499  iblcncfioo  46500  volico  46505  sublevolico  46506  volioore  46512  voliooico  46514  voliccico  46521  dirkerper  46618  dirkertrigeq  46623  dirkercncflem2  46626  fourierdlem10  46639  fourierdlem32  46661  fourierdlem33  46662  fourierdlem37  46666  fourierdlem62  46690  fourierdlem73  46701  fourierdlem74  46702  fourierdlem75  46703  fourierdlem79  46707  fourierdlem81  46709  fourierdlem82  46710  fourierdlem93  46721  fourierdlem97  46725  fourierdlem101  46729  fourierdlem103  46731  fourierdlem104  46732  sqwvfoura  46750  sqwvfourb  46751  fourierswlem  46752  fouriersw  46753  etransclem4  46760  etransclem15  46771  etransclem19  46775  etransclem20  46776  etransclem23  46779  etransclem24  46780  etransclem25  46781  etransclem27  46783  etransclem31  46787  etransclem32  46788  ioorrnopnxrlem  46828  nnfoctbdjlem  46977  isomenndlem  47052  ovn0val  47072  hoidmv0val  47105  hsphoidmvle2  47107  hoidmv1lelem1  47113  hoidmv1lelem2  47114  hoidmv1le  47116  hoidmvlelem2  47118  hoidmvlelem3  47119  ovnhoilem1  47123  hspdifhsp  47138  hoidifhspdmvle  47142  hspmbllem1  47148  hspmbllem2  47149  hspmbl  47151  volico2  47163  ovnsubadd2lem  47167  ovolval4lem2  47172  ovolval5lem1  47174  afvfundmfveq  47680  dfatafv2iota  47752  dfatafv2eqfv  47803  difmodm1lt  47907  prproropf1olem3  48059  prproropf1olem4  48060  linc1  48995  lincext3  49026  lindslinindsimp1  49027  el0ldep  49036  islindeps2  49053  itcoval0  49232  ackval0  49250