Theorem iftrue 4487

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  iftruei  4488  iftrued  4489  iftrueb  4494  ifsb  4495  ifbi  4504  ifeq2da  4514  ifeq12da  4515  ifclda  4517  ifeqda  4518  elimif  4519  ifbothda  4520  ifid  4522  ifeqor  4533  ifnot  4534  ifan  4535  ifor  4536  2if2  4537  dedth  4540  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  dfopif  4829  dfopg  4830  somin1  6126  somincom  6127  xpima1  6174  elimdelov  7516  brif1  7517  ovif12  7520  ifmpt2v  7522  tz7.44-1  8415  rdg0n  8443  resixpfo  8965  boxriin  8969  boxcutc  8970  pw2f1olem  9101  unxpdomlem2  9249  unxpdomlem3  9250  infsupprpr  9499  ordtypelem1  9513  wemaplem2  9542  unwdomg  9579  ixpiunwdom  9585  cantnfp1lem2  9681  cantnfp1lem3  9682  ssttrcl  9717  ttrclselem2  9728  acndom  10131  dfac12lem2  10224  fin23lem14  10412  axcc2lem  10515  pwfseqlem2  10745  indval2  12326  ind1  12330  uzin  13002  xrmax1  13306  xrmax2  13307  xrmin1  13308  xrmin2  13309  max1ALT  13317  max0sub  13327  ifle  13328  xmulneg1  13400  fzprval  13720  fztpval  13721  modifeq2int  14077  seqf1olem1  14185  seqf1olem2  14186  bcval2  14450  tpf1ofv0  14642  tpf1ofv1  14643  ccatval1  14723  ccatalpha  14741  swrdccat  14885  pfxccat3a  14888  swrdccat3b  14890  repswswrd  14936  cshword  14943  0csh0  14945  ccatco  14987  sgnn  15248  max0add  15478  absmax  15498  sumrblem  15878  fsumcvg  15879  summolem2a  15882  isum  15886  sumss  15891  sumss2  15893  fsumcvg2  15894  fsumser  15897  fsumsplit  15908  sumsplit  15935  prodrblem  16097  fprodcvg  16098  prodmolem2a  16102  zprod  16105  iprod  16106  iprodn0  16108  prodss  16115  fprodsplit  16134  ruclem2  16401  ruclem3  16402  flodddiv4  16586  sadadd2lem2  16621  sadcf  16624  sadc0  16625  sadcp1  16626  sadcaddlem  16628  smupf  16649  smup0  16650  gcd0val  16668  dfgcd2  16720  eucalgf  16759  eucalginv  16760  eucalglt  16761  lcmf0val  16798  phisum  16969  pc0  17033  pcgcd  17057  pcmptcl  17070  pcmpt  17071  pcmpt2  17072  pcprod  17074  fldivp1  17076  prmreclem2  17096  prmreclem4  17098  1arithlem4  17105  vdwlem6  17165  ramtcl2  17190  ramcl2  17195  ramub1lem1  17205  prmop1  17217  fvprmselelfz  17223  fvprmselgcd1  17224  ressid2  17413  xpsfrnel  17735  xpsaddlem  17746  xpsvsca  17750  mreexexd  17823  gsumval1  18873  mgm2nsgrplem2  19119  sgrp2nmndlem2  19124  symgextfve  19634  symgfixfolem1  19653  pmtrmvd  19671  pmtrfinv  19676  pmtrprfval  19702  pmtrprfvalrn  19703  frgpuptinv  19986  frgpup2  19991  frgpup3lem  19992  cyggex  20113  gsumzsplit  20142  gsummpt1n0  20180  dprdfid  20234  dmdprdsplitlem  20254  sdrgacs  21059  abvtrivd  21090  znf1o  21858  uvcvv1  22096  psrlidm  22270  psrridm  22271  mvrf1  22294  mplmonmul  22346  mplcoe1  22347  mplcoe3  22348  mplcoe5  22350  mplmon2  22371  subrgasclcl  22377  evlslem3  22390  evlslem1  22392  selvvvval  22452  psdmul  22488  psdmvr  22491  coe1tmfv1  22594  ply1sclid  22608  dmatmul  22813  scmatscmiddistr  22824  1mavmul  22864  mulmarep1gsum2  22890  1marepvmarrepid  22891  mdetdiag  22915  mdetralt2  22925  mdetunilem2  22929  mdetunilem7  22934  mdetunilem8  22935  mdetunilem9  22936  mndifsplit  22952  maducoeval2  22956  madugsum  22959  madurid  22960  gsummatr01lem3  22973  gsummatr01  22975  smadiadetglem2  22988  matunitlindflem1  22995  1elcpmat  23034  decpmatid  23089  chfacfscmulgsum  23179  chfacfpmmulgsum  23183  ptpjpre1  23891  ptbasfi  23901  ptpjopn  23932  isfcls  24329  ptcmplem2  24373  ptcmplem3  24374  tsmssplit  24472  dscmet  24892  dscopn  24893  icccmplem2  25144  iccpnfcnv  25266  xrhmeo  25268  pcopt  25344  pcopt2  25345  pcoass  25346  pcorevlem  25348  cmetcaulem  25610  ovolicc1  25838  ioorcl  25899  i1f1lem  26011  itg11  26013  itg1addlem2  26019  itg1addlem4  26021  i1fres  26027  itg1climres  26036  mbfi1fseqlem4  26040  mbfi1fseqlem5  26041  mbfi1flim  26045  itg2const2  26063  itg2seq  26064  itg2uba  26065  itg2splitlem  26070  itg2split  26071  itg2monolem1  26072  itg2cnlem1  26083  itg2cnlem2  26084  iblcnlem  26110  iblss  26126  iblss2  26127  itgitg2  26128  itgle  26131  itgss  26133  itgss2  26134  itgss3  26136  itgless  26138  ibladdlem  26141  itgaddlem1  26144  iblabslem  26149  iblabs  26150  iblabsr  26151  iblmulc2  26152  bddmulibl  26160  bddiblnc  26163  itggt0  26165  itgcn  26166  limcvallem  26192  ellimc2  26198  limccnp  26212  limccnp2  26213  limcco  26214  dvcobr  26267  dvexp2  26275  mon1pid  26473  elply2  26515  elplyd  26521  ply1termlem  26522  coe1termlem  26578  abelthlem9  26768  logtayl  26989  leibpilem2  27270  leibpi  27271  rlimcnp2  27295  efrlim  27298  igamz  27376  isnsqf  27463  mule1  27476  sqff1o  27510  muinv  27521  chtublem  27539  dchrelbasd  27567  bposlem1  27612  bposlem3  27614  bposlem5  27616  bposlem6  27617  lgsval2lem  27635  lgsneg  27649  lgsdilem  27652  lgsdir2  27658  lgsdir  27660  lgsdi  27662  lgsne0  27663  gausslemma2dlem1a  27693  2lgslem1c  27721  2lgslem3  27732  2lgs  27735  dchrvmasum2if  27825  dchrvmasumiflem1  27829  rpvmasum2  27840  pntrlog2bndlem4  27908  pntrlog2bndlem5  27909  padicabv  27958  ostth2lem4  27964  nosupno  28061  nosupbday  28063  nosupbnd1  28072  nosupbnd2  28074  noinfno  28076  noinfbday  28078  noinfbnd1  28087  maxs1  28127  maxs2  28128  mins1  28129  mins2  28130  abssid  28628  abssge0  28632  axlowdimlem15  29535  opvtxval  29582  opiedgval  29585  elimifd  33182  elim2if  33183  ifeq3da  33185  ifnefals  33187  fmptunsnop  33336  pmtridf1o  33698  fzto1stfv1  33705  resvid2  33934  psrmonmul  34225  vieta  34255  2sqr3minply  34455  cos9thpiminply  34463  xrge0iifcnv  34608  xrge0iifiso  34610  xrge0iifhom  34612  sigaclfu2  34796  ddeval1  34910  eulerpartlemb  35043  ballotlemsima  35191  ballotlemrv1  35196  signsw0glem  35225  signswmnd  35229  signswrid  35230  jaeqifi  35753  ordunmax  35758  soinfdom  35761  vonf1oonfo  35961  onf1oracwevd  35964  onprcf1of1ord  35967  indispconn  36068  ex-sategoelel  36255  ex-sategoelelomsuc  36260  ex-sategoelel12  36261  mrsubvr  36345  dfrdg2  36632  dfrdg3  36633  unisnif  36762  dfrdg4  36790  fnejoin2  37232  unbdqndv2lem2  37451  bj-xpima2sn  37946  finxpreclem1  38388  finxpreclem3  38392  poimirlem2  38616  poimirlem15  38629  poimirlem16  38630  poimirlem17  38631  poimirlem19  38633  poimirlem20  38634  poimirlem24  38638  mblfinlem2  38652  mbfposadd  38661  itg2addnclem  38665  itg2gt0cn  38669  ibladdnclem  38670  itgaddnclem1  38672  iblabsnclem  38677  iblabsnc  38678  iblmulc2nc  38679  itggt0cn  38684  ftc1anclem4  38690  ftc1anclem5  38691  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  areacirclem5  38706  areacirc  38707  fdc  38755  heiborlem4  38824  ac6s6  39180  cdleme27a  41500  cdleme31sn1  41514  cdleme31fv1  41524  cdlemk40t  42051  dihvalb  42370  sticksstones12a  43283  brif2  43354  brif12  43355  evlsbagval  43690  fsuppind  43694  dffltz  43746  pw2f1ocnv  44120  aomclem5  44136  kelac1  44141  arearect  44293  areaquad  44294  oe0rif  44363  cantnfresb  44402  safesnsupfidom1o  44494  safesnsupfilb  44495  clsk1indlem1  45121  refsum2cnlem1  46130  upbdrech2  46400  lptioo2  46719  lptioo1  46720  limsupmnfuzlem  46812  limsupre3uzlem  46821  limsup10exlem  46858  coskpi2  46952  cosknegpi  46955  cncfiooicclem1  46979  cncfiooiccre  46981  dvnxpaek  47028  dvnprodlem1  47032  dvnprodlem3  47034  itgioocnicc  47063  iblcncfioo  47064  volico  47069  sublevolico  47070  volioore  47076  voliooico  47078  voliccico  47085  dirkerper  47182  dirkertrigeq  47187  dirkercncflem2  47190  fourierdlem10  47203  fourierdlem32  47225  fourierdlem33  47226  fourierdlem37  47230  fourierdlem62  47254  fourierdlem73  47265  fourierdlem74  47266  fourierdlem75  47267  fourierdlem79  47271  fourierdlem81  47273  fourierdlem82  47274  fourierdlem93  47285  fourierdlem97  47289  fourierdlem101  47293  fourierdlem103  47295  fourierdlem104  47296  sqwvfoura  47314  sqwvfourb  47315  fourierswlem  47316  fouriersw  47317  etransclem4  47324  etransclem15  47335  etransclem19  47339  etransclem20  47340  etransclem23  47343  etransclem24  47344  etransclem25  47345  etransclem27  47347  etransclem31  47351  etransclem32  47352  ioorrnopnxrlem  47392  nnfoctbdjlem  47541  isomenndlem  47616  ovn0val  47636  hoidmv0val  47669  hsphoidmvle2  47671  hoidmv1lelem1  47677  hoidmv1lelem2  47678  hoidmv1le  47680  hoidmvlelem2  47682  hoidmvlelem3  47683  ovnhoilem1  47687  hspdifhsp  47702  hoidifhspdmvle  47706  hspmbllem1  47712  hspmbllem2  47713  hspmbl  47715  volico2  47727  ovnsubadd2lem  47731  ovolval4lem2  47736  ovolval5lem1  47738  afvfundmfveq  48284  dfatafv2iota  48356  dfatafv2eqfv  48407  difmodm1lt  48511  prproropf1olem3  48663  prproropf1olem4  48664  linc1  49613  lincext3  49644  lindslinindsimp1  49645  el0ldep  49654  islindeps2  49671  itcoval0  49850  ackval0  49868  crosspv1d  51036  crosspv2d  51037  veronesev1lem  51049  veronesev2lem  51050  veronesev3lem  51051  veronesev4lem  51052  veronesev5lem  51053  veronesev6lem  51054  veronesevrowd  51055