Theorem iftrue 4466

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 4462	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1041	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	abbi2dv 2878	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2798	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {cab 2716  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  iftruei  4467  iftrued  4468  ifsb  4473  ifbi  4482  ifeq2da  4492  ifeq12da  4493  ifclda  4495  ifeqda  4496  elimif  4497  ifbothda  4498  ifid  4500  ifeqor  4511  ifnot  4512  ifan  4513  ifor  4514  2if2  4515  dedth  4518  elimhyp  4525  elimhyp2v  4526  elimhyp3v  4527  elimhyp4v  4528  elimdhyp  4530  keephyp2v  4532  keephyp3v  4533  dfopifOLD  4802  dfopg  4803  somin1  6043  somincom  6044  xpima1  6091  elimdelov  7380  ovif12  7383  tz7.44-1  8246  rdg0n  8274  resixpfo  8733  boxriin  8737  boxcutc  8738  pw2f1olem  8872  unxpdomlem2  9037  unxpdomlem3  9038  infsupprpr  9272  ordtypelem1  9286  wemaplem2  9315  unwdomg  9352  ixpiunwdom  9358  cantnfp1lem2  9446  cantnfp1lem3  9447  ssttrcl  9482  ttrclselem2  9493  acndom  9816  dfac12lem2  9909  fin23lem14  10098  axcc2lem  10201  pwfseqlem2  10424  uzin  12627  xrmax1  12918  xrmax2  12919  xrmin1  12920  xrmin2  12921  max1ALT  12929  max0sub  12939  ifle  12940  xmulneg1  13012  fzprval  13326  fztpval  13327  modifeq2int  13662  seqf1olem1  13771  seqf1olem2  13772  bcval2  14028  ccatval1  14290  ccatval1OLD  14291  ccatalpha  14307  swrdccat  14457  pfxccat3a  14460  swrdccat3b  14462  repswswrd  14506  cshword  14513  0csh0  14515  ccatco  14557  sgnn  14814  max0add  15031  absmax  15050  sumrblem  15432  fsumcvg  15433  summolem2a  15436  isum  15440  sumss  15445  sumss2  15447  fsumcvg2  15448  fsumser  15451  fsumsplit  15462  sumsplit  15489  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  zprod  15656  iprod  15657  iprodn0  15659  prodss  15666  fprodsplit  15685  ruclem2  15950  ruclem3  15951  flodddiv4  16131  sadadd2lem2  16166  sadcf  16169  sadc0  16170  sadcp1  16171  sadcaddlem  16173  smupf  16194  smup0  16195  gcd0val  16213  dfgcd2  16263  eucalgf  16297  eucalginv  16298  eucalglt  16299  lcmf0val  16336  phisum  16500  pc0  16564  pcgcd  16588  pcmptcl  16601  pcmpt  16602  pcmpt2  16603  pcprod  16605  fldivp1  16607  prmreclem2  16627  prmreclem4  16629  1arithlem4  16636  vdwlem6  16696  ramtcl2  16721  ramcl2  16726  ramub1lem1  16736  prmop1  16748  fvprmselelfz  16754  fvprmselgcd1  16755  ressid2  16954  xpsfrnel  17282  xpsaddlem  17293  xpsvsca  17297  mreexexd  17366  gsumval1  18376  mgm2nsgrplem2  18567  sgrp2nmndlem2  18572  symgextfve  19036  symgfixfolem1  19055  pmtrmvd  19073  pmtrfinv  19078  pmtrprfval  19104  pmtrprfvalrn  19105  frgpuptinv  19386  frgpup2  19391  frgpup3lem  19392  cyggex  19508  gsumzsplit  19537  gsummpt1n0  19575  dprdfid  19629  dmdprdsplitlem  19649  sdrgacs  20078  abvtrivd  20109  znf1o  20768  uvcvv1  21005  psrlidm  21181  psrridm  21182  mvrf1  21203  mplmonmul  21246  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  mplmon2  21278  subrgasclcl  21284  evlslem3  21299  evlslem1  21301  coe1tmfv1  21454  ply1sclid  21468  dmatmul  21655  scmatscmiddistr  21666  1mavmul  21706  mulmarep1gsum2  21732  1marepvmarrepid  21733  mdetdiag  21757  mdetralt2  21767  mdetunilem2  21771  mdetunilem7  21776  mdetunilem8  21777  mdetunilem9  21778  mndifsplit  21794  maducoeval2  21798  madugsum  21801  madurid  21802  gsummatr01lem3  21815  gsummatr01  21817  smadiadetglem2  21830  1elcpmat  21873  decpmatid  21928  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  ptpjpre1  22731  ptbasfi  22741  ptpjopn  22772  isfcls  23169  ptcmplem2  23213  ptcmplem3  23214  tsmssplit  23312  dscmet  23737  dscopn  23738  icccmplem2  23995  iccpnfcnv  24116  xrhmeo  24118  pcopt  24194  pcopt2  24195  pcoass  24196  pcorevlem  24198  cmetcaulem  24461  ovolicc1  24689  ioorcl  24750  i1f1lem  24862  itg11  24864  itg1addlem2  24870  itg1addlem4  24872  itg1addlem4OLD  24873  i1fres  24879  itg1climres  24888  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1flim  24897  itg2const2  24915  itg2seq  24916  itg2uba  24917  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2cnlem1  24935  itg2cnlem2  24936  iblcnlem  24962  iblss  24978  iblss2  24979  itgitg2  24980  itgle  24983  itgss  24985  itgss2  24986  itgss3  24988  itgless  24990  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  bddmulibl  25012  bddiblnc  25015  itggt0  25017  itgcn  25018  limcvallem  25044  ellimc2  25050  limccnp  25064  limccnp2  25065  limcco  25066  dvcobr  25119  dvexp2  25127  elply2  25366  elplyd  25372  ply1termlem  25373  coe1termlem  25428  abelthlem9  25608  logtayl  25824  leibpilem2  26100  leibpi  26101  rlimcnp2  26125  efrlim  26128  igamz  26206  isnsqf  26293  mule1  26306  sqff1o  26340  muinv  26351  chtublem  26368  dchrelbasd  26396  bposlem1  26441  bposlem3  26443  bposlem5  26445  bposlem6  26446  lgsval2lem  26464  lgsneg  26478  lgsdilem  26481  lgsdir2  26487  lgsdir  26489  lgsdi  26491  lgsne0  26492  gausslemma2dlem1a  26522  2lgslem1c  26550  2lgslem3  26561  2lgs  26564  dchrvmasum2if  26654  dchrvmasumiflem1  26658  rpvmasum2  26669  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  padicabv  26787  ostth2lem4  26793  axlowdimlem15  27333  opvtxval  27382  opiedgval  27385  elimifd  30895  elim2if  30896  ifeq3da  30898  pmtridf1o  31370  fzto1stfv1  31377  resvid2  31536  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  indval2  31991  ind1  31994  sigaclfu2  32098  ddeval1  32211  eulerpartlemb  32344  ballotlemsima  32491  ballotlemrv1  32496  signsw0glem  32541  signswmnd  32545  signswrid  32546  indispconn  33205  ex-sategoelel  33392  ex-sategoelelomsuc  33397  ex-sategoelel12  33398  mrsubvr  33482  dfrdg2  33780  dfrdg3  33781  nosupno  33915  nosupbday  33917  nosupbnd1  33926  nosupbnd2  33928  noinfno  33930  noinfbday  33932  noinfbnd1  33941  unisnif  34236  dfrdg4  34262  fnejoin2  34567  unbdqndv2lem2  34699  bj-xpima2sn  35157  finxpreclem1  35569  finxpreclem3  35573  matunitlindflem1  35782  poimirlem2  35788  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem24  35810  mblfinlem2  35824  mbfposadd  35833  itg2addnclem  35837  itg2gt0cn  35841  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itggt0cn  35856  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirclem5  35878  areacirc  35879  fdc  35912  heiborlem4  35981  ac6s6  36339  cdleme27a  38388  cdleme31sn1  38402  cdleme31fv1  38412  cdlemk40t  38939  dihvalb  39258  sticksstones12a  40120  metakunt5  40136  metakunt6  40137  metakunt10  40141  metakunt11  40142  metakunt20  40151  brif1  40205  brif2  40206  brif12  40207  evlsbagval  40282  fsuppind  40286  dffltz  40478  pw2f1ocnv  40866  aomclem5  40890  kelac1  40895  mon1pid  41037  arearect  41053  areaquad  41054  clsk1indlem1  41662  refsum2cnlem1  42587  upbdrech2  42854  lptioo2  43179  lptioo1  43180  limsupmnfuzlem  43274  limsupre3uzlem  43283  limsup10exlem  43320  coskpi2  43414  cosknegpi  43417  cncfiooicclem1  43441  cncfiooiccre  43443  dvnxpaek  43490  dvnprodlem1  43494  dvnprodlem3  43496  itgioocnicc  43525  iblcncfioo  43526  volico  43531  sublevolico  43532  volioore  43538  voliooico  43540  voliccico  43547  dirkerper  43644  dirkertrigeq  43649  dirkercncflem2  43652  fourierdlem10  43665  fourierdlem32  43687  fourierdlem33  43688  fourierdlem37  43692  fourierdlem62  43716  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem93  43747  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  etransclem4  43786  etransclem15  43797  etransclem19  43801  etransclem20  43802  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem31  43813  etransclem32  43814  ioorrnopnxrlem  43854  nnfoctbdjlem  44000  isomenndlem  44075  ovn0val  44095  hoidmv0val  44128  hsphoidmvle2  44130  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1le  44139  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  hspdifhsp  44161  hoidifhspdmvle  44165  hspmbllem1  44171  hspmbllem2  44172  hspmbl  44174  volico2  44186  ovnsubadd2lem  44190  ovolval4lem2  44195  ovolval5lem1  44197  afvfundmfveq  44641  dfatafv2iota  44713  dfatafv2eqfv  44764  prproropf1olem3  44968  prproropf1olem4  44969  linc1  45777  lincext3  45808  lindslinindsimp1  45809  el0ldep  45818  islindeps2  45835  itcoval0  46019  ackval0  46037