Theorem iftrue 4473

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  iftruei  4474  iftrued  4475  iftrueb  4480  ifsb  4481  ifbi  4490  ifeq2da  4500  ifeq12da  4501  ifclda  4503  ifeqda  4504  elimif  4505  ifbothda  4506  ifid  4508  ifeqor  4519  ifnot  4520  ifan  4521  ifor  4522  2if2  4523  dedth  4526  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elimdhyp  4538  keephyp2v  4540  keephyp3v  4541  dfopif  4814  dfopg  4815  somin1  6088  somincom  6089  xpima1  6139  elimdelov  7454  brif1  7455  ovif12  7458  ifmpt2v  7460  tz7.44-1  8336  rdg0n  8364  resixpfo  8875  boxriin  8879  boxcutc  8880  pw2f1olem  9010  unxpdomlem2  9158  unxpdomlem3  9159  infsupprpr  9410  ordtypelem1  9424  wemaplem2  9453  unwdomg  9490  ixpiunwdom  9496  cantnfp1lem2  9589  cantnfp1lem3  9590  ssttrcl  9625  ttrclselem2  9636  acndom  9962  dfac12lem2  10056  fin23lem14  10244  axcc2lem  10347  pwfseqlem2  10571  indval2  12153  ind1  12157  uzin  12813  xrmax1  13116  xrmax2  13117  xrmin1  13118  xrmin2  13119  max1ALT  13127  max0sub  13137  ifle  13138  xmulneg1  13210  fzprval  13528  fztpval  13529  modifeq2int  13884  seqf1olem1  13992  seqf1olem2  13993  bcval2  14256  tpf1ofv0  14447  tpf1ofv1  14448  ccatval1  14528  ccatalpha  14545  swrdccat  14686  pfxccat3a  14689  swrdccat3b  14691  repswswrd  14735  cshword  14742  0csh0  14744  ccatco  14786  sgnn  15045  max0add  15261  absmax  15281  sumrblem  15662  fsumcvg  15663  summolem2a  15666  isum  15670  sumss  15675  sumss2  15677  fsumcvg2  15678  fsumser  15681  fsumsplit  15692  sumsplit  15719  prodrblem  15883  fprodcvg  15884  prodmolem2a  15888  zprod  15891  iprod  15892  iprodn0  15894  prodss  15901  fprodsplit  15920  ruclem2  16188  ruclem3  16189  flodddiv4  16373  sadadd2lem2  16408  sadcf  16411  sadc0  16412  sadcp1  16413  sadcaddlem  16415  smupf  16436  smup0  16437  gcd0val  16455  dfgcd2  16504  eucalgf  16541  eucalginv  16542  eucalglt  16543  lcmf0val  16580  phisum  16750  pc0  16814  pcgcd  16838  pcmptcl  16851  pcmpt  16852  pcmpt2  16853  pcprod  16855  fldivp1  16857  prmreclem2  16877  prmreclem4  16879  1arithlem4  16886  vdwlem6  16946  ramtcl2  16971  ramcl2  16976  ramub1lem1  16986  prmop1  16998  fvprmselelfz  17004  fvprmselgcd1  17005  ressid2  17193  xpsfrnel  17515  xpsaddlem  17526  xpsvsca  17530  mreexexd  17603  gsumval1  18640  mgm2nsgrplem2  18879  sgrp2nmndlem2  18884  symgextfve  19383  symgfixfolem1  19402  pmtrmvd  19420  pmtrfinv  19425  pmtrprfval  19451  pmtrprfvalrn  19452  frgpuptinv  19735  frgpup2  19740  frgpup3lem  19741  cyggex  19862  gsumzsplit  19891  gsummpt1n0  19929  dprdfid  19983  dmdprdsplitlem  20003  sdrgacs  20767  abvtrivd  20798  znf1o  21539  uvcvv1  21777  psrlidm  21949  psrridm  21950  mvrf1  21973  mplmonmul  22023  mplcoe1  22024  mplcoe3  22025  mplcoe5  22027  mplmon2  22048  subrgasclcl  22054  evlslem3  22067  evlslem1  22069  psdmul  22141  psdmvr  22144  coe1tmfv1  22248  ply1sclid  22262  dmatmul  22471  scmatscmiddistr  22482  1mavmul  22522  mulmarep1gsum2  22548  1marepvmarrepid  22549  mdetdiag  22573  mdetralt2  22583  mdetunilem2  22587  mdetunilem7  22592  mdetunilem8  22593  mdetunilem9  22594  mndifsplit  22610  maducoeval2  22614  madugsum  22617  madurid  22618  gsummatr01lem3  22631  gsummatr01  22633  smadiadetglem2  22646  1elcpmat  22689  decpmatid  22744  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  ptpjpre1  23545  ptbasfi  23555  ptpjopn  23586  isfcls  23983  ptcmplem2  24027  ptcmplem3  24028  tsmssplit  24126  dscmet  24546  dscopn  24547  icccmplem2  24798  iccpnfcnv  24920  xrhmeo  24922  pcopt  24998  pcopt2  24999  pcoass  25000  pcorevlem  25002  cmetcaulem  25264  ovolicc1  25492  ioorcl  25553  i1f1lem  25665  itg11  25667  itg1addlem2  25673  itg1addlem4  25675  i1fres  25681  itg1climres  25690  mbfi1fseqlem4  25694  mbfi1fseqlem5  25695  mbfi1flim  25699  itg2const2  25717  itg2seq  25718  itg2uba  25719  itg2splitlem  25724  itg2split  25725  itg2monolem1  25726  itg2cnlem1  25737  itg2cnlem2  25738  iblcnlem  25765  iblss  25781  iblss2  25782  itgitg2  25783  itgle  25786  itgss  25788  itgss2  25789  itgss3  25791  itgless  25793  ibladdlem  25796  itgaddlem1  25799  iblabslem  25804  iblabs  25805  iblabsr  25806  iblmulc2  25807  bddmulibl  25815  bddiblnc  25818  itggt0  25820  itgcn  25821  limcvallem  25847  ellimc2  25853  limccnp  25867  limccnp2  25868  limcco  25869  dvcobr  25922  dvexp2  25930  mon1pid  26131  elply2  26173  elplyd  26179  ply1termlem  26180  coe1termlem  26235  abelthlem9  26421  logtayl  26640  leibpilem2  26922  leibpi  26923  rlimcnp2  26947  efrlim  26950  efrlimOLD  26951  igamz  27029  isnsqf  27116  mule1  27129  sqff1o  27163  muinv  27174  chtublem  27193  dchrelbasd  27221  bposlem1  27266  bposlem3  27268  bposlem5  27270  bposlem6  27271  lgsval2lem  27289  lgsneg  27303  lgsdilem  27306  lgsdir2  27312  lgsdir  27314  lgsdi  27316  lgsne0  27317  gausslemma2dlem1a  27347  2lgslem1c  27375  2lgslem3  27386  2lgs  27389  dchrvmasum2if  27479  dchrvmasumiflem1  27483  rpvmasum2  27494  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  padicabv  27612  ostth2lem4  27618  nosupno  27686  nosupbday  27688  nosupbnd1  27697  nosupbnd2  27699  noinfno  27701  noinfbday  27703  noinfbnd1  27712  maxs1  27752  maxs2  27753  mins1  27754  mins2  27755  abssid  28252  abssge0  28256  axlowdimlem15  29044  opvtxval  29091  opiedgval  29094  elimifd  32633  elim2if  32634  ifeq3da  32636  ifnefals  32638  fmptunsnop  32793  pmtridf1o  33175  fzto1stfv1  33182  resvid2  33410  psrmonmul  33714  vieta  33744  2sqr3minply  33945  cos9thpiminply  33953  xrge0iifcnv  34098  xrge0iifiso  34100  xrge0iifhom  34102  sigaclfu2  34286  ddeval1  34399  eulerpartlemb  34533  ballotlemsima  34681  ballotlemrv1  34686  signsw0glem  34718  signswmnd  34722  signswrid  34723  indispconn  35437  ex-sategoelel  35624  ex-sategoelelomsuc  35629  ex-sategoelel12  35630  mrsubvr  35714  dfrdg2  35996  dfrdg3  35997  unisnif  36126  dfrdg4  36154  fnejoin2  36572  unbdqndv2lem2  36783  bj-xpima2sn  37278  finxpreclem1  37716  finxpreclem3  37720  matunitlindflem1  37948  poimirlem2  37954  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem19  37971  poimirlem20  37972  poimirlem24  37976  mblfinlem2  37990  mbfposadd  37999  itg2addnclem  38003  itg2gt0cn  38007  ibladdnclem  38008  itgaddnclem1  38010  iblabsnclem  38015  iblabsnc  38016  iblmulc2nc  38017  itggt0cn  38022  ftc1anclem4  38028  ftc1anclem5  38029  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  areacirclem5  38044  areacirc  38045  fdc  38077  heiborlem4  38146  ac6s6  38504  cdleme27a  40824  cdleme31sn1  40838  cdleme31fv1  40848  cdlemk40t  41375  dihvalb  41694  sticksstones12a  42607  brif2  42676  brif12  42677  evlsbagval  43013  selvvvval  43029  fsuppind  43034  dffltz  43078  pw2f1ocnv  43480  aomclem5  43501  kelac1  43506  arearect  43658  areaquad  43659  oe0rif  43728  cantnfresb  43767  safesnsupfidom1o  43859  safesnsupfilb  43860  clsk1indlem1  44487  refsum2cnlem1  45483  upbdrech2  45756  lptioo2  46076  lptioo1  46077  limsupmnfuzlem  46169  limsupre3uzlem  46178  limsup10exlem  46215  coskpi2  46309  cosknegpi  46312  cncfiooicclem1  46336  cncfiooiccre  46338  dvnxpaek  46385  dvnprodlem1  46389  dvnprodlem3  46391  itgioocnicc  46420  iblcncfioo  46421  volico  46426  sublevolico  46427  volioore  46433  voliooico  46435  voliccico  46442  dirkerper  46539  dirkertrigeq  46544  dirkercncflem2  46547  fourierdlem10  46560  fourierdlem32  46582  fourierdlem33  46583  fourierdlem37  46587  fourierdlem62  46611  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem93  46642  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  etransclem4  46681  etransclem15  46692  etransclem19  46696  etransclem20  46697  etransclem23  46700  etransclem24  46701  etransclem25  46702  etransclem27  46704  etransclem31  46708  etransclem32  46709  ioorrnopnxrlem  46749  nnfoctbdjlem  46898  isomenndlem  46973  ovn0val  46993  hoidmv0val  47026  hsphoidmvle2  47028  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1le  47037  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem1  47044  hspdifhsp  47059  hoidifhspdmvle  47063  hspmbllem1  47069  hspmbllem2  47070  hspmbl  47072  volico2  47084  ovnsubadd2lem  47088  ovolval4lem2  47093  ovolval5lem1  47095  afvfundmfveq  47583  dfatafv2iota  47655  dfatafv2eqfv  47706  difmodm1lt  47810  prproropf1olem3  47962  prproropf1olem4  47963  linc1  48898  lincext3  48929  lindslinindsimp1  48930  el0ldep  48939  islindeps2  48956  itcoval0  49135  ackval0  49153