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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {cab 2709  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  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  4821  dfopg  4822  somin1  6085  somincom  6086  xpima1  6136  elimdelov  7448  brif1  7449  ovif12  7452  ifmpt2v  7454  tz7.44-1  8331  rdg0n  8359  resixpfo  8866  boxriin  8870  boxcutc  8871  pw2f1olem  9000  unxpdomlem2  9147  unxpdomlem3  9148  infsupprpr  9396  ordtypelem1  9410  wemaplem2  9439  unwdomg  9476  ixpiunwdom  9482  cantnfp1lem2  9575  cantnfp1lem3  9576  ssttrcl  9611  ttrclselem2  9622  acndom  9948  dfac12lem2  10042  fin23lem14  10230  axcc2lem  10333  pwfseqlem2  10556  uzin  12778  xrmax1  13080  xrmax2  13081  xrmin1  13082  xrmin2  13083  max1ALT  13091  max0sub  13101  ifle  13102  xmulneg1  13174  fzprval  13491  fztpval  13492  modifeq2int  13846  seqf1olem1  13954  seqf1olem2  13955  bcval2  14218  tpf1ofv0  14409  tpf1ofv1  14410  ccatval1  14490  ccatalpha  14507  swrdccat  14648  pfxccat3a  14651  swrdccat3b  14653  repswswrd  14697  cshword  14704  0csh0  14706  ccatco  14748  sgnn  15007  max0add  15223  absmax  15243  sumrblem  15624  fsumcvg  15625  summolem2a  15628  isum  15632  sumss  15637  sumss2  15639  fsumcvg2  15640  fsumser  15643  fsumsplit  15654  sumsplit  15681  prodrblem  15842  fprodcvg  15843  prodmolem2a  15847  zprod  15850  iprod  15851  iprodn0  15853  prodss  15860  fprodsplit  15879  ruclem2  16147  ruclem3  16148  flodddiv4  16332  sadadd2lem2  16367  sadcf  16370  sadc0  16371  sadcp1  16372  sadcaddlem  16374  smupf  16395  smup0  16396  gcd0val  16414  dfgcd2  16463  eucalgf  16500  eucalginv  16501  eucalglt  16502  lcmf0val  16539  phisum  16708  pc0  16772  pcgcd  16796  pcmptcl  16809  pcmpt  16810  pcmpt2  16811  pcprod  16813  fldivp1  16815  prmreclem2  16835  prmreclem4  16837  1arithlem4  16844  vdwlem6  16904  ramtcl2  16929  ramcl2  16934  ramub1lem1  16944  prmop1  16956  fvprmselelfz  16962  fvprmselgcd1  16963  ressid2  17151  xpsfrnel  17472  xpsaddlem  17483  xpsvsca  17487  mreexexd  17560  gsumval1  18597  mgm2nsgrplem2  18833  sgrp2nmndlem2  18838  symgextfve  19337  symgfixfolem1  19356  pmtrmvd  19374  pmtrfinv  19379  pmtrprfval  19405  pmtrprfvalrn  19406  frgpuptinv  19689  frgpup2  19694  frgpup3lem  19695  cyggex  19816  gsumzsplit  19845  gsummpt1n0  19883  dprdfid  19937  dmdprdsplitlem  19957  sdrgacs  20722  abvtrivd  20753  znf1o  21494  uvcvv1  21732  psrlidm  21905  psrridm  21906  mvrf1  21929  mplmonmul  21977  mplcoe1  21978  mplcoe3  21979  mplcoe5  21981  mplmon2  22002  subrgasclcl  22008  evlslem3  22021  evlslem1  22023  psdmul  22087  psdmvr  22090  coe1tmfv1  22194  ply1sclid  22208  dmatmul  22418  scmatscmiddistr  22429  1mavmul  22469  mulmarep1gsum2  22495  1marepvmarrepid  22496  mdetdiag  22520  mdetralt2  22530  mdetunilem2  22534  mdetunilem7  22539  mdetunilem8  22540  mdetunilem9  22541  mndifsplit  22557  maducoeval2  22561  madugsum  22564  madurid  22565  gsummatr01lem3  22578  gsummatr01  22580  smadiadetglem2  22593  1elcpmat  22636  decpmatid  22691  chfacfscmulgsum  22781  chfacfpmmulgsum  22785  ptpjpre1  23492  ptbasfi  23502  ptpjopn  23533  isfcls  23930  ptcmplem2  23974  ptcmplem3  23975  tsmssplit  24073  dscmet  24493  dscopn  24494  icccmplem2  24745  iccpnfcnv  24875  xrhmeo  24877  pcopt  24955  pcopt2  24956  pcoass  24957  pcorevlem  24959  cmetcaulem  25221  ovolicc1  25450  ioorcl  25511  i1f1lem  25623  itg11  25625  itg1addlem2  25631  itg1addlem4  25633  i1fres  25639  itg1climres  25648  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfi1flim  25657  itg2const2  25675  itg2seq  25676  itg2uba  25677  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itg2cnlem1  25695  itg2cnlem2  25696  iblcnlem  25723  iblss  25739  iblss2  25740  itgitg2  25741  itgle  25744  itgss  25746  itgss2  25747  itgss3  25749  itgless  25751  ibladdlem  25754  itgaddlem1  25757  iblabslem  25762  iblabs  25763  iblabsr  25764  iblmulc2  25765  bddmulibl  25773  bddiblnc  25776  itggt0  25778  itgcn  25779  limcvallem  25805  ellimc2  25811  limccnp  25825  limccnp2  25826  limcco  25827  dvcobr  25882  dvcobrOLD  25883  dvexp2  25891  mon1pid  26092  elply2  26134  elplyd  26140  ply1termlem  26141  coe1termlem  26196  abelthlem9  26383  logtayl  26602  leibpilem2  26884  leibpi  26885  rlimcnp2  26909  efrlim  26912  efrlimOLD  26913  igamz  26991  isnsqf  27078  mule1  27091  sqff1o  27125  muinv  27136  chtublem  27155  dchrelbasd  27183  bposlem1  27228  bposlem3  27230  bposlem5  27232  bposlem6  27233  lgsval2lem  27251  lgsneg  27265  lgsdilem  27268  lgsdir2  27274  lgsdir  27276  lgsdi  27278  lgsne0  27279  gausslemma2dlem1a  27309  2lgslem1c  27337  2lgslem3  27348  2lgs  27351  dchrvmasum2if  27441  dchrvmasumiflem1  27445  rpvmasum2  27456  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  padicabv  27574  ostth2lem4  27580  nosupno  27648  nosupbday  27650  nosupbnd1  27659  nosupbnd2  27661  noinfno  27663  noinfbday  27665  noinfbnd1  27674  maxs1  27710  maxs2  27711  mins1  27712  mins2  27713  abssid  28185  abssge0  28189  axlowdimlem15  28941  opvtxval  28988  opiedgval  28991  elimifd  32530  elim2if  32531  ifeq3da  32533  ifnefals  32535  fmptunsnop  32688  indval2  32842  ind1  32845  pmtridf1o  33070  fzto1stfv1  33077  resvid2  33302  2sqr3minply  33800  cos9thpiminply  33808  xrge0iifcnv  33953  xrge0iifiso  33955  xrge0iifhom  33957  sigaclfu2  34141  ddeval1  34254  eulerpartlemb  34388  ballotlemsima  34536  ballotlemrv1  34541  signsw0glem  34573  signswmnd  34577  signswrid  34578  indispconn  35285  ex-sategoelel  35472  ex-sategoelelomsuc  35477  ex-sategoelel12  35478  mrsubvr  35562  dfrdg2  35844  dfrdg3  35845  unisnif  35974  dfrdg4  36002  fnejoin2  36420  unbdqndv2lem2  36561  bj-xpima2sn  37009  finxpreclem1  37440  finxpreclem3  37444  matunitlindflem1  37662  poimirlem2  37668  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem24  37690  mblfinlem2  37704  mbfposadd  37713  itg2addnclem  37717  itg2gt0cn  37721  ibladdnclem  37722  itgaddnclem1  37724  iblabsnclem  37729  iblabsnc  37730  iblmulc2nc  37731  itggt0cn  37736  ftc1anclem4  37742  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  areacirclem5  37758  areacirc  37759  fdc  37791  heiborlem4  37860  ac6s6  38218  cdleme27a  40472  cdleme31sn1  40486  cdleme31fv1  40496  cdlemk40t  41023  dihvalb  41342  sticksstones12a  42256  brif2  42323  brif12  42324  evlsbagval  42665  selvvvval  42684  fsuppind  42689  dffltz  42733  pw2f1ocnv  43135  aomclem5  43156  kelac1  43161  arearect  43313  areaquad  43314  oe0rif  43383  cantnfresb  43422  safesnsupfidom1o  43515  safesnsupfilb  43516  clsk1indlem1  44143  refsum2cnlem1  45139  upbdrech2  45414  lptioo2  45736  lptioo1  45737  limsupmnfuzlem  45829  limsupre3uzlem  45838  limsup10exlem  45875  coskpi2  45969  cosknegpi  45972  cncfiooicclem1  45996  cncfiooiccre  45998  dvnxpaek  46045  dvnprodlem1  46049  dvnprodlem3  46051  itgioocnicc  46080  iblcncfioo  46081  volico  46086  sublevolico  46087  volioore  46093  voliooico  46095  voliccico  46102  dirkerper  46199  dirkertrigeq  46204  dirkercncflem2  46207  fourierdlem10  46220  fourierdlem32  46242  fourierdlem33  46243  fourierdlem37  46247  fourierdlem62  46271  fourierdlem73  46282  fourierdlem74  46283  fourierdlem75  46284  fourierdlem79  46288  fourierdlem81  46290  fourierdlem82  46291  fourierdlem93  46302  fourierdlem97  46306  fourierdlem101  46310  fourierdlem103  46312  fourierdlem104  46313  sqwvfoura  46331  sqwvfourb  46332  fourierswlem  46333  fouriersw  46334  etransclem4  46341  etransclem15  46352  etransclem19  46356  etransclem20  46357  etransclem23  46360  etransclem24  46361  etransclem25  46362  etransclem27  46364  etransclem31  46368  etransclem32  46369  ioorrnopnxrlem  46409  nnfoctbdjlem  46558  isomenndlem  46633  ovn0val  46653  hoidmv0val  46686  hsphoidmvle2  46688  hoidmv1lelem1  46694  hoidmv1lelem2  46695  hoidmv1le  46697  hoidmvlelem2  46699  hoidmvlelem3  46700  ovnhoilem1  46704  hspdifhsp  46719  hoidifhspdmvle  46723  hspmbllem1  46729  hspmbllem2  46730  hspmbl  46732  volico2  46744  ovnsubadd2lem  46748  ovolval4lem2  46753  ovolval5lem1  46755  afvfundmfveq  47243  dfatafv2iota  47315  dfatafv2eqfv  47366  difmodm1lt  47464  prproropf1olem3  47610  prproropf1olem4  47611  linc1  48531  lincext3  48562  lindslinindsimp1  48563  el0ldep  48572  islindeps2  48589  itcoval0  48768  ackval0  48786