Theorem iftrue 4506

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  ifcif 4500

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  iftruei  4507  iftrued  4508  iftrueb  4513  ifsb  4514  ifbi  4523  ifeq2da  4533  ifeq12da  4534  ifclda  4536  ifeqda  4537  elimif  4538  ifbothda  4539  ifid  4541  ifeqor  4552  ifnot  4553  ifan  4554  ifor  4555  2if2  4556  dedth  4559  elimhyp  4566  elimhyp2v  4567  elimhyp3v  4568  elimhyp4v  4569  elimdhyp  4571  keephyp2v  4573  keephyp3v  4574  dfopif  4846  dfopg  4847  somin1  6122  somincom  6123  xpima1  6172  elimdelov  7501  brif1  7502  ovif12  7505  ifmpt2v  7507  tz7.44-1  8418  rdg0n  8446  resixpfo  8948  boxriin  8952  boxcutc  8953  pw2f1olem  9088  unxpdomlem2  9257  unxpdomlem3  9258  infsupprpr  9516  ordtypelem1  9530  wemaplem2  9559  unwdomg  9596  ixpiunwdom  9602  cantnfp1lem2  9691  cantnfp1lem3  9692  ssttrcl  9727  ttrclselem2  9738  acndom  10063  dfac12lem2  10157  fin23lem14  10345  axcc2lem  10448  pwfseqlem2  10671  uzin  12890  xrmax1  13189  xrmax2  13190  xrmin1  13191  xrmin2  13192  max1ALT  13200  max0sub  13210  ifle  13211  xmulneg1  13283  fzprval  13600  fztpval  13601  modifeq2int  13949  seqf1olem1  14057  seqf1olem2  14058  bcval2  14321  tpf1ofv0  14512  tpf1ofv1  14513  ccatval1  14593  ccatalpha  14609  swrdccat  14751  pfxccat3a  14754  swrdccat3b  14756  repswswrd  14800  cshword  14807  0csh0  14809  ccatco  14852  sgnn  15111  max0add  15327  absmax  15346  sumrblem  15725  fsumcvg  15726  summolem2a  15729  isum  15733  sumss  15738  sumss2  15740  fsumcvg2  15741  fsumser  15744  fsumsplit  15755  sumsplit  15782  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  zprod  15951  iprod  15952  iprodn0  15954  prodss  15961  fprodsplit  15980  ruclem2  16248  ruclem3  16249  flodddiv4  16432  sadadd2lem2  16467  sadcf  16470  sadc0  16471  sadcp1  16472  sadcaddlem  16474  smupf  16495  smup0  16496  gcd0val  16514  dfgcd2  16563  eucalgf  16600  eucalginv  16601  eucalglt  16602  lcmf0val  16639  phisum  16808  pc0  16872  pcgcd  16896  pcmptcl  16909  pcmpt  16910  pcmpt2  16911  pcprod  16913  fldivp1  16915  prmreclem2  16935  prmreclem4  16937  1arithlem4  16944  vdwlem6  17004  ramtcl2  17029  ramcl2  17034  ramub1lem1  17044  prmop1  17056  fvprmselelfz  17062  fvprmselgcd1  17063  ressid2  17253  xpsfrnel  17574  xpsaddlem  17585  xpsvsca  17589  mreexexd  17658  gsumval1  18659  mgm2nsgrplem2  18895  sgrp2nmndlem2  18900  symgextfve  19398  symgfixfolem1  19417  pmtrmvd  19435  pmtrfinv  19440  pmtrprfval  19466  pmtrprfvalrn  19467  frgpuptinv  19750  frgpup2  19755  frgpup3lem  19756  cyggex  19877  gsumzsplit  19906  gsummpt1n0  19944  dprdfid  19998  dmdprdsplitlem  20018  sdrgacs  20759  abvtrivd  20790  znf1o  21510  uvcvv1  21747  psrlidm  21920  psrridm  21921  mvrf1  21944  mplmonmul  21992  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mplmon2  22017  subrgasclcl  22023  evlslem3  22036  evlslem1  22038  psdmul  22102  psdmvr  22105  coe1tmfv1  22209  ply1sclid  22223  dmatmul  22433  scmatscmiddistr  22444  1mavmul  22484  mulmarep1gsum2  22510  1marepvmarrepid  22511  mdetdiag  22535  mdetralt2  22545  mdetunilem2  22549  mdetunilem7  22554  mdetunilem8  22555  mdetunilem9  22556  mndifsplit  22572  maducoeval2  22576  madugsum  22579  madurid  22580  gsummatr01lem3  22593  gsummatr01  22595  smadiadetglem2  22608  1elcpmat  22651  decpmatid  22706  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  ptpjpre1  23507  ptbasfi  23517  ptpjopn  23548  isfcls  23945  ptcmplem2  23989  ptcmplem3  23990  tsmssplit  24088  dscmet  24509  dscopn  24510  icccmplem2  24761  iccpnfcnv  24891  xrhmeo  24893  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  cmetcaulem  25238  ovolicc1  25467  ioorcl  25528  i1f1lem  25640  itg11  25642  itg1addlem2  25648  itg1addlem4  25650  i1fres  25656  itg1climres  25665  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1flim  25674  itg2const2  25692  itg2seq  25693  itg2uba  25694  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2cnlem1  25712  itg2cnlem2  25713  iblcnlem  25740  iblss  25756  iblss2  25757  itgitg2  25758  itgle  25761  itgss  25763  itgss2  25764  itgss3  25766  itgless  25768  ibladdlem  25771  itgaddlem1  25774  iblabslem  25779  iblabs  25780  iblabsr  25781  iblmulc2  25782  bddmulibl  25790  bddiblnc  25793  itggt0  25795  itgcn  25796  limcvallem  25822  ellimc2  25828  limccnp  25842  limccnp2  25843  limcco  25844  dvcobr  25899  dvcobrOLD  25900  dvexp2  25908  mon1pid  26109  elply2  26151  elplyd  26157  ply1termlem  26158  coe1termlem  26213  abelthlem9  26400  logtayl  26619  leibpilem2  26901  leibpi  26902  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  igamz  27008  isnsqf  27095  mule1  27108  sqff1o  27142  muinv  27153  chtublem  27172  dchrelbasd  27200  bposlem1  27245  bposlem3  27247  bposlem5  27249  bposlem6  27250  lgsval2lem  27268  lgsneg  27282  lgsdilem  27285  lgsdir2  27291  lgsdir  27293  lgsdi  27295  lgsne0  27296  gausslemma2dlem1a  27326  2lgslem1c  27354  2lgslem3  27365  2lgs  27368  dchrvmasum2if  27458  dchrvmasumiflem1  27462  rpvmasum2  27473  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  padicabv  27591  ostth2lem4  27597  nosupno  27665  nosupbday  27667  nosupbnd1  27676  nosupbnd2  27678  noinfno  27680  noinfbday  27682  noinfbnd1  27691  maxs1  27727  maxs2  27728  mins1  27729  mins2  27730  abssid  28182  abssge0  28186  axlowdimlem15  28881  opvtxval  28928  opiedgval  28931  elimifd  32470  elim2if  32471  ifeq3da  32473  ifnefals  32475  fmptunsnop  32623  indval2  32777  ind1  32780  pmtridf1o  33051  fzto1stfv1  33058  resvid2  33292  2sqr3minply  33760  cos9thpiminply  33768  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  sigaclfu2  34098  ddeval1  34211  eulerpartlemb  34346  ballotlemsima  34494  ballotlemrv1  34499  signsw0glem  34531  signswmnd  34535  signswrid  34536  indispconn  35202  ex-sategoelel  35389  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  mrsubvr  35479  dfrdg2  35759  dfrdg3  35760  unisnif  35889  dfrdg4  35915  fnejoin2  36333  unbdqndv2lem2  36474  bj-xpima2sn  36922  finxpreclem1  37353  finxpreclem3  37357  matunitlindflem1  37586  poimirlem2  37592  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  mblfinlem2  37628  mbfposadd  37637  itg2addnclem  37641  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem1  37648  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  itggt0cn  37660  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  areacirclem5  37682  areacirc  37683  fdc  37715  heiborlem4  37784  ac6s6  38142  cdleme27a  40332  cdleme31sn1  40346  cdleme31fv1  40356  cdlemk40t  40883  dihvalb  41202  sticksstones12a  42116  metakunt5  42168  metakunt6  42169  metakunt10  42173  metakunt11  42174  metakunt20  42183  brif2  42221  brif12  42222  evlsbagval  42536  selvvvval  42555  fsuppind  42560  dffltz  42604  pw2f1ocnv  43008  aomclem5  43029  kelac1  43034  arearect  43186  areaquad  43187  oe0rif  43256  cantnfresb  43295  safesnsupfidom1o  43388  safesnsupfilb  43389  clsk1indlem1  44016  refsum2cnlem1  45009  upbdrech2  45285  lptioo2  45608  lptioo1  45609  limsupmnfuzlem  45703  limsupre3uzlem  45712  limsup10exlem  45749  coskpi2  45843  cosknegpi  45846  cncfiooicclem1  45870  cncfiooiccre  45872  dvnxpaek  45919  dvnprodlem1  45923  dvnprodlem3  45925  itgioocnicc  45954  iblcncfioo  45955  volico  45960  sublevolico  45961  volioore  45967  voliooico  45969  voliccico  45976  dirkerper  46073  dirkertrigeq  46078  dirkercncflem2  46081  fourierdlem10  46094  fourierdlem32  46116  fourierdlem33  46117  fourierdlem37  46121  fourierdlem62  46145  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem93  46176  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem4  46215  etransclem15  46226  etransclem19  46230  etransclem20  46231  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem27  46238  etransclem31  46242  etransclem32  46243  ioorrnopnxrlem  46283  nnfoctbdjlem  46432  isomenndlem  46507  ovn0val  46527  hoidmv0val  46560  hsphoidmvle2  46562  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem1  46578  hspdifhsp  46593  hoidifhspdmvle  46597  hspmbllem1  46603  hspmbllem2  46604  hspmbl  46606  volico2  46618  ovnsubadd2lem  46622  ovolval4lem2  46627  ovolval5lem1  46629  afvfundmfveq  47115  dfatafv2iota  47187  dfatafv2eqfv  47238  prproropf1olem3  47467  prproropf1olem4  47468  linc1  48349  lincext3  48380  lindslinindsimp1  48381  el0ldep  48390  islindeps2  48407  itcoval0  48590  ackval0  48608