Theorem iftrue 4497

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2708  ifcif 4491

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  iftruei  4498  iftrued  4499  iftrueb  4504  ifsb  4505  ifbi  4514  ifeq2da  4524  ifeq12da  4525  ifclda  4527  ifeqda  4528  elimif  4529  ifbothda  4530  ifid  4532  ifeqor  4543  ifnot  4544  ifan  4545  ifor  4546  2if2  4547  dedth  4550  elimhyp  4557  elimhyp2v  4558  elimhyp3v  4559  elimhyp4v  4560  elimdhyp  4562  keephyp2v  4564  keephyp3v  4565  dfopif  4837  dfopg  4838  somin1  6109  somincom  6110  xpima1  6159  elimdelov  7488  brif1  7489  ovif12  7492  ifmpt2v  7494  tz7.44-1  8377  rdg0n  8405  resixpfo  8912  boxriin  8916  boxcutc  8917  pw2f1olem  9050  unxpdomlem2  9205  unxpdomlem3  9206  infsupprpr  9464  ordtypelem1  9478  wemaplem2  9507  unwdomg  9544  ixpiunwdom  9550  cantnfp1lem2  9639  cantnfp1lem3  9640  ssttrcl  9675  ttrclselem2  9686  acndom  10011  dfac12lem2  10105  fin23lem14  10293  axcc2lem  10396  pwfseqlem2  10619  uzin  12840  xrmax1  13142  xrmax2  13143  xrmin1  13144  xrmin2  13145  max1ALT  13153  max0sub  13163  ifle  13164  xmulneg1  13236  fzprval  13553  fztpval  13554  modifeq2int  13905  seqf1olem1  14013  seqf1olem2  14014  bcval2  14277  tpf1ofv0  14468  tpf1ofv1  14469  ccatval1  14549  ccatalpha  14565  swrdccat  14707  pfxccat3a  14710  swrdccat3b  14712  repswswrd  14756  cshword  14763  0csh0  14765  ccatco  14808  sgnn  15067  max0add  15283  absmax  15303  sumrblem  15684  fsumcvg  15685  summolem2a  15688  isum  15692  sumss  15697  sumss2  15699  fsumcvg2  15700  fsumser  15703  fsumsplit  15714  sumsplit  15741  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  iprod  15911  iprodn0  15913  prodss  15920  fprodsplit  15939  ruclem2  16207  ruclem3  16208  flodddiv4  16392  sadadd2lem2  16427  sadcf  16430  sadc0  16431  sadcp1  16432  sadcaddlem  16434  smupf  16455  smup0  16456  gcd0val  16474  dfgcd2  16523  eucalgf  16560  eucalginv  16561  eucalglt  16562  lcmf0val  16599  phisum  16768  pc0  16832  pcgcd  16856  pcmptcl  16869  pcmpt  16870  pcmpt2  16871  pcprod  16873  fldivp1  16875  prmreclem2  16895  prmreclem4  16897  1arithlem4  16904  vdwlem6  16964  ramtcl2  16989  ramcl2  16994  ramub1lem1  17004  prmop1  17016  fvprmselelfz  17022  fvprmselgcd1  17023  ressid2  17211  xpsfrnel  17532  xpsaddlem  17543  xpsvsca  17547  mreexexd  17616  gsumval1  18617  mgm2nsgrplem2  18853  sgrp2nmndlem2  18858  symgextfve  19356  symgfixfolem1  19375  pmtrmvd  19393  pmtrfinv  19398  pmtrprfval  19424  pmtrprfvalrn  19425  frgpuptinv  19708  frgpup2  19713  frgpup3lem  19714  cyggex  19835  gsumzsplit  19864  gsummpt1n0  19902  dprdfid  19956  dmdprdsplitlem  19976  sdrgacs  20717  abvtrivd  20748  znf1o  21468  uvcvv1  21705  psrlidm  21878  psrridm  21879  mvrf1  21902  mplmonmul  21950  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  mplmon2  21975  subrgasclcl  21981  evlslem3  21994  evlslem1  21996  psdmul  22060  psdmvr  22063  coe1tmfv1  22167  ply1sclid  22181  dmatmul  22391  scmatscmiddistr  22402  1mavmul  22442  mulmarep1gsum2  22468  1marepvmarrepid  22469  mdetdiag  22493  mdetralt2  22503  mdetunilem2  22507  mdetunilem7  22512  mdetunilem8  22513  mdetunilem9  22514  mndifsplit  22530  maducoeval2  22534  madugsum  22537  madurid  22538  gsummatr01lem3  22551  gsummatr01  22553  smadiadetglem2  22566  1elcpmat  22609  decpmatid  22664  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  ptpjpre1  23465  ptbasfi  23475  ptpjopn  23506  isfcls  23903  ptcmplem2  23947  ptcmplem3  23948  tsmssplit  24046  dscmet  24467  dscopn  24468  icccmplem2  24719  iccpnfcnv  24849  xrhmeo  24851  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  cmetcaulem  25195  ovolicc1  25424  ioorcl  25485  i1f1lem  25597  itg11  25599  itg1addlem2  25605  itg1addlem4  25607  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1flim  25631  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2cnlem1  25669  itg2cnlem2  25670  iblcnlem  25697  iblss  25713  iblss2  25714  itgitg2  25715  itgle  25718  itgss  25720  itgss2  25721  itgss3  25723  itgless  25725  ibladdlem  25728  itgaddlem1  25731  iblabslem  25736  iblabs  25737  iblabsr  25738  iblmulc2  25739  bddmulibl  25747  bddiblnc  25750  itggt0  25752  itgcn  25753  limcvallem  25779  ellimc2  25785  limccnp  25799  limccnp2  25800  limcco  25801  dvcobr  25856  dvcobrOLD  25857  dvexp2  25865  mon1pid  26066  elply2  26108  elplyd  26114  ply1termlem  26115  coe1termlem  26170  abelthlem9  26357  logtayl  26576  leibpilem2  26858  leibpi  26859  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  igamz  26965  isnsqf  27052  mule1  27065  sqff1o  27099  muinv  27110  chtublem  27129  dchrelbasd  27157  bposlem1  27202  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgsval2lem  27225  lgsneg  27239  lgsdilem  27242  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsne0  27253  gausslemma2dlem1a  27283  2lgslem1c  27311  2lgslem3  27322  2lgs  27325  dchrvmasum2if  27415  dchrvmasumiflem1  27419  rpvmasum2  27430  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  padicabv  27548  ostth2lem4  27554  nosupno  27622  nosupbday  27624  nosupbnd1  27633  nosupbnd2  27635  noinfno  27637  noinfbday  27639  noinfbnd1  27648  maxs1  27684  maxs2  27685  mins1  27686  mins2  27687  abssid  28150  abssge0  28154  axlowdimlem15  28890  opvtxval  28937  opiedgval  28940  elimifd  32479  elim2if  32480  ifeq3da  32482  ifnefals  32484  fmptunsnop  32630  indval2  32784  ind1  32787  pmtridf1o  33058  fzto1stfv1  33065  resvid2  33309  2sqr3minply  33777  cos9thpiminply  33785  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  sigaclfu2  34118  ddeval1  34231  eulerpartlemb  34366  ballotlemsima  34514  ballotlemrv1  34519  signsw0glem  34551  signswmnd  34555  signswrid  34556  indispconn  35228  ex-sategoelel  35415  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  mrsubvr  35505  dfrdg2  35790  dfrdg3  35791  unisnif  35920  dfrdg4  35946  fnejoin2  36364  unbdqndv2lem2  36505  bj-xpima2sn  36953  finxpreclem1  37384  finxpreclem3  37388  matunitlindflem1  37617  poimirlem2  37623  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  mblfinlem2  37659  mbfposadd  37668  itg2addnclem  37672  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem1  37679  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  itggt0cn  37691  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirclem5  37713  areacirc  37714  fdc  37746  heiborlem4  37815  ac6s6  38173  cdleme27a  40368  cdleme31sn1  40382  cdleme31fv1  40392  cdlemk40t  40919  dihvalb  41238  sticksstones12a  42152  brif2  42219  brif12  42220  evlsbagval  42561  selvvvval  42580  fsuppind  42585  dffltz  42629  pw2f1ocnv  43033  aomclem5  43054  kelac1  43059  arearect  43211  areaquad  43212  oe0rif  43281  cantnfresb  43320  safesnsupfidom1o  43413  safesnsupfilb  43414  clsk1indlem1  44041  refsum2cnlem1  45038  upbdrech2  45313  lptioo2  45636  lptioo1  45637  limsupmnfuzlem  45731  limsupre3uzlem  45740  limsup10exlem  45777  coskpi2  45871  cosknegpi  45874  cncfiooicclem1  45898  cncfiooiccre  45900  dvnxpaek  45947  dvnprodlem1  45951  dvnprodlem3  45953  itgioocnicc  45982  iblcncfioo  45983  volico  45988  sublevolico  45989  volioore  45995  voliooico  45997  voliccico  46004  dirkerper  46101  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem10  46122  fourierdlem32  46144  fourierdlem33  46145  fourierdlem37  46149  fourierdlem62  46173  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem93  46204  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem4  46243  etransclem15  46254  etransclem19  46258  etransclem20  46259  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem27  46266  etransclem31  46270  etransclem32  46271  ioorrnopnxrlem  46311  nnfoctbdjlem  46460  isomenndlem  46535  ovn0val  46555  hoidmv0val  46588  hsphoidmvle2  46590  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  hspdifhsp  46621  hoidifhspdmvle  46625  hspmbllem1  46631  hspmbllem2  46632  hspmbl  46634  volico2  46646  ovnsubadd2lem  46650  ovolval4lem2  46655  ovolval5lem1  46657  afvfundmfveq  47143  dfatafv2iota  47215  dfatafv2eqfv  47266  difmodm1lt  47364  prproropf1olem3  47510  prproropf1olem4  47511  linc1  48418  lincext3  48449  lindslinindsimp1  48450  el0ldep  48459  islindeps2  48476  itcoval0  48655  ackval0  48673