Theorem iftrue 4494

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  ifcif 4488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  iftruei  4495  iftrued  4496  iftrueb  4501  ifsb  4502  ifbi  4511  ifeq2da  4521  ifeq12da  4522  ifclda  4524  ifeqda  4525  elimif  4526  ifbothda  4527  ifid  4529  ifeqor  4540  ifnot  4541  ifan  4542  ifor  4543  2if2  4544  dedth  4547  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  dfopif  4834  dfopg  4835  somin1  6106  somincom  6107  xpima1  6156  elimdelov  7485  brif1  7486  ovif12  7489  ifmpt2v  7491  tz7.44-1  8374  rdg0n  8402  resixpfo  8909  boxriin  8913  boxcutc  8914  pw2f1olem  9045  unxpdomlem2  9198  unxpdomlem3  9199  infsupprpr  9457  ordtypelem1  9471  wemaplem2  9500  unwdomg  9537  ixpiunwdom  9543  cantnfp1lem2  9632  cantnfp1lem3  9633  ssttrcl  9668  ttrclselem2  9679  acndom  10004  dfac12lem2  10098  fin23lem14  10286  axcc2lem  10389  pwfseqlem2  10612  uzin  12833  xrmax1  13135  xrmax2  13136  xrmin1  13137  xrmin2  13138  max1ALT  13146  max0sub  13156  ifle  13157  xmulneg1  13229  fzprval  13546  fztpval  13547  modifeq2int  13898  seqf1olem1  14006  seqf1olem2  14007  bcval2  14270  tpf1ofv0  14461  tpf1ofv1  14462  ccatval1  14542  ccatalpha  14558  swrdccat  14700  pfxccat3a  14703  swrdccat3b  14705  repswswrd  14749  cshword  14756  0csh0  14758  ccatco  14801  sgnn  15060  max0add  15276  absmax  15296  sumrblem  15677  fsumcvg  15678  summolem2a  15681  isum  15685  sumss  15690  sumss2  15692  fsumcvg2  15693  fsumser  15696  fsumsplit  15707  sumsplit  15734  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  iprod  15904  iprodn0  15906  prodss  15913  fprodsplit  15932  ruclem2  16200  ruclem3  16201  flodddiv4  16385  sadadd2lem2  16420  sadcf  16423  sadc0  16424  sadcp1  16425  sadcaddlem  16427  smupf  16448  smup0  16449  gcd0val  16467  dfgcd2  16516  eucalgf  16553  eucalginv  16554  eucalglt  16555  lcmf0val  16592  phisum  16761  pc0  16825  pcgcd  16849  pcmptcl  16862  pcmpt  16863  pcmpt2  16864  pcprod  16866  fldivp1  16868  prmreclem2  16888  prmreclem4  16890  1arithlem4  16897  vdwlem6  16957  ramtcl2  16982  ramcl2  16987  ramub1lem1  16997  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  ressid2  17204  xpsfrnel  17525  xpsaddlem  17536  xpsvsca  17540  mreexexd  17609  gsumval1  18610  mgm2nsgrplem2  18846  sgrp2nmndlem2  18851  symgextfve  19349  symgfixfolem1  19368  pmtrmvd  19386  pmtrfinv  19391  pmtrprfval  19417  pmtrprfvalrn  19418  frgpuptinv  19701  frgpup2  19706  frgpup3lem  19707  cyggex  19828  gsumzsplit  19857  gsummpt1n0  19895  dprdfid  19949  dmdprdsplitlem  19969  sdrgacs  20710  abvtrivd  20741  znf1o  21461  uvcvv1  21698  psrlidm  21871  psrridm  21872  mvrf1  21895  mplmonmul  21943  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  mplmon2  21968  subrgasclcl  21974  evlslem3  21987  evlslem1  21989  psdmul  22053  psdmvr  22056  coe1tmfv1  22160  ply1sclid  22174  dmatmul  22384  scmatscmiddistr  22395  1mavmul  22435  mulmarep1gsum2  22461  1marepvmarrepid  22462  mdetdiag  22486  mdetralt2  22496  mdetunilem2  22500  mdetunilem7  22505  mdetunilem8  22506  mdetunilem9  22507  mndifsplit  22523  maducoeval2  22527  madugsum  22530  madurid  22531  gsummatr01lem3  22544  gsummatr01  22546  smadiadetglem2  22559  1elcpmat  22602  decpmatid  22657  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  ptpjpre1  23458  ptbasfi  23468  ptpjopn  23499  isfcls  23896  ptcmplem2  23940  ptcmplem3  23941  tsmssplit  24039  dscmet  24460  dscopn  24461  icccmplem2  24712  iccpnfcnv  24842  xrhmeo  24844  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  cmetcaulem  25188  ovolicc1  25417  ioorcl  25478  i1f1lem  25590  itg11  25592  itg1addlem2  25598  itg1addlem4  25600  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1flim  25624  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2cnlem1  25662  itg2cnlem2  25663  iblcnlem  25690  iblss  25706  iblss2  25707  itgitg2  25708  itgle  25711  itgss  25713  itgss2  25714  itgss3  25716  itgless  25718  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddmulibl  25740  bddiblnc  25743  itggt0  25745  itgcn  25746  limcvallem  25772  ellimc2  25778  limccnp  25792  limccnp2  25793  limcco  25794  dvcobr  25849  dvcobrOLD  25850  dvexp2  25858  mon1pid  26059  elply2  26101  elplyd  26107  ply1termlem  26108  coe1termlem  26163  abelthlem9  26350  logtayl  26569  leibpilem2  26851  leibpi  26852  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  igamz  26958  isnsqf  27045  mule1  27058  sqff1o  27092  muinv  27103  chtublem  27122  dchrelbasd  27150  bposlem1  27195  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgsval2lem  27218  lgsneg  27232  lgsdilem  27235  lgsdir2  27241  lgsdir  27243  lgsdi  27245  lgsne0  27246  gausslemma2dlem1a  27276  2lgslem1c  27304  2lgslem3  27315  2lgs  27318  dchrvmasum2if  27408  dchrvmasumiflem1  27412  rpvmasum2  27423  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  padicabv  27541  ostth2lem4  27547  nosupno  27615  nosupbday  27617  nosupbnd1  27626  nosupbnd2  27628  noinfno  27630  noinfbday  27632  noinfbnd1  27641  maxs1  27677  maxs2  27678  mins1  27679  mins2  27680  abssid  28143  abssge0  28147  axlowdimlem15  28883  opvtxval  28930  opiedgval  28933  elimifd  32472  elim2if  32473  ifeq3da  32475  ifnefals  32477  fmptunsnop  32623  indval2  32777  ind1  32780  pmtridf1o  33051  fzto1stfv1  33058  resvid2  33302  2sqr3minply  33770  cos9thpiminply  33778  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  sigaclfu2  34111  ddeval1  34224  eulerpartlemb  34359  ballotlemsima  34507  ballotlemrv1  34512  signsw0glem  34544  signswmnd  34548  signswrid  34549  indispconn  35221  ex-sategoelel  35408  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  mrsubvr  35498  dfrdg2  35783  dfrdg3  35784  unisnif  35913  dfrdg4  35939  fnejoin2  36357  unbdqndv2lem2  36498  bj-xpima2sn  36946  finxpreclem1  37377  finxpreclem3  37381  matunitlindflem1  37610  poimirlem2  37616  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  mblfinlem2  37652  mbfposadd  37661  itg2addnclem  37665  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  itggt0cn  37684  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem5  37706  areacirc  37707  fdc  37739  heiborlem4  37808  ac6s6  38166  cdleme27a  40361  cdleme31sn1  40375  cdleme31fv1  40385  cdlemk40t  40912  dihvalb  41231  sticksstones12a  42145  brif2  42212  brif12  42213  evlsbagval  42554  selvvvval  42573  fsuppind  42578  dffltz  42622  pw2f1ocnv  43026  aomclem5  43047  kelac1  43052  arearect  43204  areaquad  43205  oe0rif  43274  cantnfresb  43313  safesnsupfidom1o  43406  safesnsupfilb  43407  clsk1indlem1  44034  refsum2cnlem1  45031  upbdrech2  45306  lptioo2  45629  lptioo1  45630  limsupmnfuzlem  45724  limsupre3uzlem  45733  limsup10exlem  45770  coskpi2  45864  cosknegpi  45867  cncfiooicclem1  45891  cncfiooiccre  45893  dvnxpaek  45940  dvnprodlem1  45944  dvnprodlem3  45946  itgioocnicc  45975  iblcncfioo  45976  volico  45981  sublevolico  45982  volioore  45988  voliooico  45990  voliccico  45997  dirkerper  46094  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem10  46115  fourierdlem32  46137  fourierdlem33  46138  fourierdlem37  46142  fourierdlem62  46166  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem4  46236  etransclem15  46247  etransclem19  46251  etransclem20  46252  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem31  46263  etransclem32  46264  ioorrnopnxrlem  46304  nnfoctbdjlem  46453  isomenndlem  46528  ovn0val  46548  hoidmv0val  46581  hsphoidmvle2  46583  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  hspdifhsp  46614  hoidifhspdmvle  46618  hspmbllem1  46624  hspmbllem2  46625  hspmbl  46627  volico2  46639  ovnsubadd2lem  46643  ovolval4lem2  46648  ovolval5lem1  46650  afvfundmfveq  47139  dfatafv2iota  47211  dfatafv2eqfv  47262  difmodm1lt  47360  prproropf1olem3  47506  prproropf1olem4  47507  linc1  48414  lincext3  48445  lindslinindsimp1  48446  el0ldep  48455  islindeps2  48472  itcoval0  48651  ackval0  48669