Theorem eleqtrrd 2832

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eleqtrrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2736	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2831	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  3eltr4d  2844  rspc2vd  3913  disjxiun  5107  eldmressnsn  5998  fnsnbg  7141  elimdelov  7488  elovmpt3rab1  7652  fnwelem  8113  tfrlem13  8361  tz7.44-2  8378  omordi  8533  oneo  8548  omeulem2  8550  oeordi  8554  oeeui  8569  nnneo  8622  naddelim  8653  erref  8694  en1uniel  9003  omxpenlem  9047  unblem3  9248  dffi3  9389  ordtypelem10  9487  oismo  9500  cantnff  9634  cantnfp1lem3  9640  cantnflem1  9649  cnfcom  9660  r1ordg  9738  r1pwss  9744  rankwflemb  9753  r1elwf  9756  rankidb  9760  rankonidlem  9788  fseqenlem2  9985  dfac12lem1  10104  dfac12lem2  10105  pwsdompw  10163  ackbij2lem3  10200  ackbij2  10202  cfsmolem  10230  hsmexlem4  10389  ttukeylem3  10471  ttukeylem7  10475  iundom2g  10500  fpwwe2lem8  10598  canthwelem  10610  pwfseqlem4  10622  winalim2  10656  r1wunlim  10697  tskmid  10800  fzopth  13529  predfz  13621  fzoss2  13655  fz1fzo0m1  13678  fzo0addel  13686  fzo0addelr  13687  elfzoext  13690  fzosubel3  13694  elfzomin  13705  elfzonlteqm1  13709  fzoend  13725  fzoopth  13730  fzofzp1  13732  fzofzp1b  13733  peano2fzor  13742  zmodfzo  13863  seqf1olem2  14014  bcn2  14291  swrdccat2  14641  pfxccat1  14674  swrdswrd  14677  pfxccatin12  14705  splfv1  14727  revcl  14733  revlen  14734  revccat  14738  revrev  14739  repswpfx  14757  cshwidxmod  14775  revco  14807  limsupgre  15454  summolem2a  15688  fsumm1  15724  fsumcom2  15747  prodmolem2a  15907  fprodm1  15940  fprodcom2  15957  prmreclem4  16897  prmreclem5  16898  vdwapid1  16953  vdwlem5  16963  vdwlem8  16966  vdwnnlem2  16974  ramub1lem1  17004  ramub1lem2  17005  mrieqvlemd  17597  mreexd  17610  mreexexlemd  17612  catcocl  17653  catass  17654  moni  17705  epii  17712  inviso1  17735  episect  17754  invisoinvl  17759  catsubcat  17808  subccocl  17814  fullsubc  17819  funcco  17840  resf2nd  17864  funcres  17865  fthepi  17899  nati  17927  arwhoma  18014  catccatid  18075  resscatc  18078  catcisolem  18079  catcoppccl  18086  catcfuccl  18087  estrreslem2  18106  funcestrcsetclem3  18110  funcestrcsetclem8  18115  equivestrcsetc  18120  funcsetcestrclem3  18124  funcsetcestrclem8  18130  xpcco  18151  xpcco2  18155  xpccatid  18156  prfcl  18171  catcxpccl  18175  curf12  18195  curf1cl  18196  curf2  18197  curf2cl  18199  curfcl  18200  uncf2  18205  uncfcurf  18207  diag12  18212  diag2  18213  curf2ndf  18215  hofcl  18227  oppchofcl  18228  oyoncl  18238  yonedalem3a  18242  yonedalem4b  18244  yonedalem22  18246  yonedalem3b  18247  yonedalem3  18248  yonedainv  18249  yonffthlem  18250  latcl2  18402  latlem  18403  latjcom  18413  latmcom  18429  clatlem  18468  clatlubcl2  18470  clatglbcl2  18472  acsfiindd  18519  gsumpropd2lem  18613  sgrppropd  18665  mndpropd  18693  imasmnd  18709  frmdmnd  18793  frmdgsum  18796  grpsubpropd2  18985  imasgrp  18995  subg0  19071  0ghm  19169  resghm2  19172  ghmco  19175  pwsdiagghm  19183  ghmqusnsglem2  19220  ghmqusnsg  19221  ghmquskerlem2  19224  ghmquskerlem3  19225  ghmqusker  19226  psgnunilem1  19430  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  sylow1lem4  19538  sylow1lem5  19539  efglem  19653  efgtf  19659  efginvrel2  19664  efginvrel1  19665  efgsdmi  19669  efgs1b  19673  efgsres  19675  efgsfo  19676  efgredleme  19680  efgredlemc  19682  efgredlem  19684  efgcpbllemb  19692  frgp0  19697  frgpadd  19700  frgpinv  19701  vrgpf  19705  vrgpinv  19706  frgpuplem  19709  frgpup1  19712  frgpup2  19713  frgpup3lem  19714  frgpnabllem1  19810  frgpnabllem2  19811  gsumval3  19844  dprdfid  19956  dprdsn  19975  dprd2da  19981  dpjidcl  19997  pgpfac1lem2  20014  pgpfaclem3  20022  ablsimpg1gend  20044  ablsimpgprmd  20054  rngpropd  20090  imasrng  20093  ringpropd  20204  imasring  20246  qusring2  20250  pwsco1rhm  20418  pwsco2rhm  20419  lringuplu  20460  subrgunit  20506  pwsdiagrhm  20523  rnghmsubcsetclem1  20547  zrinitorngc  20558  zrtermorngc  20559  zrzeroorngc  20560  rhmsubcsetclem1  20576  rhmsubcrngclem1  20582  zrtermoringc  20591  zrninitoringc  20592  srhmsubclem2  20594  srhmsubc  20596  cntzsdrg  20718  isabvd  20728  lmodprop2d  20837  islssd  20848  prdsvscacl  20881  prdslmodd  20882  islmhm2  20952  lmhmco  20957  lmhmplusg  20958  lmhmvsca  20959  lmhmpropd  20987  lsppreli  21004  ellspsn4  21041  lssacsex  21061  lspsnat  21062  lidlnsg  21165  qus2idrng  21190  qus1  21191  qusrhm  21193  rhmpreimaidl  21194  rhmqusnsg  21202  rngqiprngghmlem1  21204  rngqiprngfulem1  21228  irinitoringc  21396  nzerooringczr  21397  znf1o  21468  cssmre  21609  dsmmlss  21660  frlmsplit2  21689  frlmbas3  21692  frlmup1  21714  assapropd  21788  psr0cl  21868  psrnegcl  21870  psr1cl  21877  resspsrmul  21892  subrgpsr  21894  mvrf  21901  mplmon  21949  mplcoe1  21951  subrgasclcl  21981  mplind  21984  evlslem1  21996  subrgply1  22124  psrplusgpropd  22127  ply1coe  22192  cply1coe0bi  22196  lply1binomsc  22205  ply1fermltlchr  22206  evls1val  22214  evls1rhm  22216  evl1val  22223  evl1rhm  22226  pf1ind  22249  evl1scvarpw  22257  evls1fpws  22263  mhmcompl  22274  rhmply1  22280  matbas2i  22316  matplusg2  22321  matvsca2  22322  matsubgcell  22328  matvscacell  22330  mpomatmul  22340  mavmulval  22439  mavmulcl  22441  mavmulass  22443  mavmul0  22446  mavmumamul1  22449  m1detdiag  22491  cramerimplem2  22578  mat2pmatmul  22625  mat2pmatlin  22629  monmatcollpw  22673  pmatcollpwfi  22676  mply1topmatcl  22699  pm2mpghm  22710  pm2mpmhmlem2  22713  pm2mp  22719  chpmat1dlem  22729  chpmat1d  22730  chpdmatlem0  22731  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  chfacfscmulcl  22751  cpmadugsumlemB  22768  cpmadugsumlemC  22769  chcoeffeqlem  22779  cldmreon  22988  neiptopreu  23027  maxlp  23041  ordttopon  23087  ordtrest2lem  23097  cnprcl2  23145  lmcnp  23198  resthauslem  23257  hauscmplem  23300  1stcfb  23339  2ndcctbss  23349  2ndcomap  23352  dis2ndc  23354  loclly  23381  hausllycmp  23388  locfincmp  23420  dissnref  23422  kgeni  23431  kgenidm  23441  ptpjpre2  23474  xkoopn  23483  txopn  23496  ptpjopn  23506  ptcldmpt  23508  ptcls  23510  pthaus  23532  txkgen  23546  xkohaus  23547  xkopt  23549  txconn  23583  imastps  23615  kqid  23622  kqopn  23628  kqcld  23629  isr0  23631  indishmph  23692  pt1hmeo  23700  ptuncnv  23701  ptunhmeo  23702  t0kq  23712  filconn  23777  uzrest  23791  uffixsn  23819  fmfnfmlem2  23849  flimss2  23866  flimss1  23867  flimclslem  23878  flfcnp  23898  fclsfnflim  23921  uffclsflim  23925  fcfelbas  23930  alexsublem  23938  alexsub  23939  cnextcn  23961  cnextfres1  23962  cnextfres  23963  tmdgsum  23989  distgp  23993  indistgp  23994  symgtgp  24000  ghmcnp  24009  qustgpopn  24014  qustgplem  24015  qustgphaus  24017  prdstmdd  24018  prdstgpd  24019  tsmsid  24034  tsmssubm  24037  tsmsmhm  24040  tsmsadd  24041  tsmssplit  24046  utop2nei  24145  utop3cls  24146  neipcfilu  24190  cnextucn  24197  ucnextcn  24198  blpnfctr  24331  lpbl  24398  met2ndci  24417  tmsxps  24431  metcnpi  24439  metcnpi2  24440  metcnpi3  24441  metustid  24449  metustsym  24450  metustexhalf  24451  subgngp  24530  ngptgp  24531  sranlm  24579  nlmvscn  24582  nrginvrcn  24587  lssnlm  24596  nghmcn  24640  iccntr  24717  icccmplem2  24719  msdcn  24737  cncfmptc  24812  cncfmptid  24813  cncfmpt2f  24815  icoopnst  24843  iocopnst  24844  nmoleub2lem3  25022  nmoleub3  25026  nmhmcn  25027  ipcn  25153  cfilfcls  25181  caucfil  25190  equivcau  25207  caubl  25215  flimcfil  25221  cmssmscld  25257  rrxdstprj1  25316  minveclem3b  25335  minveclem4  25339  mulcncf  25353  ovolicc2lem3  25427  ovolicc2lem4  25428  opnmbllem  25509  vitalilem2  25517  mbfsup  25572  mbfinf  25573  mbfi1fseqlem4  25626  limccnp  25799  limccnp2  25800  dvreslem  25817  dvres2lem  25818  dvidlem  25823  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmul  25854  dvcof  25859  dvcnvlem  25887  dvef  25891  rollelem  25900  dvlip2  25907  dvivthlem1  25920  dvivth  25922  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  ply1rem  26078  fta1blem  26083  plycpn  26204  plyrem  26220  tayl0  26276  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem3  26318  psercn  26343  pserdv  26346  abelth  26358  efabl  26466  efopnlem1  26572  loglesqrt  26678  relogbf  26708  efrlim  26886  efrlimOLD  26887  dchrghm  27174  dchrptlem3  27184  nodenselem5  27607  nosupres  27626  noinfres  27641  sltlpss  27826  precsexlem11  28126  noseq0  28191  noseqp1  28192  noseqrdgfn  28207  noseqrdgsuc  28209  tgbtwntriv2  28421  tgbtwnne  28424  ercgrg  28451  tgidinside  28505  tgbtwnconn1  28509  tglnne  28562  tglnne0  28574  tglnpt2  28575  tglineneq  28578  ncolncol  28580  coltr3  28582  mirln  28610  mirln2  28611  mirconn  28612  krippenlem  28624  footexALT  28652  footexlem1  28653  footexlem2  28654  colperpexlem3  28666  mideulem2  28668  opphllem  28669  oppne3  28677  opphllem1  28681  opphllem2  28682  opphllem4  28684  oppperpex  28687  opphl  28688  hlpasch  28690  hpgerlem  28699  colhp  28704  midbtwn  28713  lmieu  28718  lmiisolem  28730  sacgr  28765  f1otrg  28805  f1otrge  28806  ebtwntg  28916  ecgrtg  28917  eengtrkg  28920  eengtrkge  28921  upgr1eop  29049  usgredg3  29150  uspgr1eop  29181  usgr1eop  29184  vtxdun  29416  vtxdfiun  29417  1loopgruspgr  29435  1loopgrvd2  29438  1hevtxdg1  29441  1egrvtxdg1  29444  1egrvtxdg0  29446  umgr2v2e  29460  wlkres  29605  wlkp1lem4  29611  wlkp1  29616  cyclnumvtx  29737  wwlksm1edg  29818  wwlksnext  29830  wwlksnextproplem3  29848  clwwlkel  29982  1wlkdlem2  30074  trlsegvdeg  30163  eupth2lem3lem1  30164  eupth2lem3lem2  30165  extwwlkfab  30288  numclwlk2lem2f  30313  spansnid  31499  elspansn4  31509  fnpreimac  32602  ccatf1  32877  ccatws1f1olast  32881  swrdrn2  32883  swrdrn3  32884  swrdf1  32885  splfv3  32887  pwrssmgc  32933  pfxchn  32942  chnind  32944  chnub  32945  chnlt  32946  wrdpmtrlast  33057  psgnfzto1stlem  33064  cycpmfv1  33077  cycpmfv2  33078  cycpmco2lem2  33091  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  cyc3co2  33104  cycpmrn  33107  submarchi  33147  subrdom  33242  fracfld  33265  imaslmod  33331  quslmod  33336  quslmhm  33337  nsgqusf1olem2  33392  lmhmqusker  33395  rhmquskerlem  33403  idlinsubrg  33409  drngidl  33411  rhmpreimaprmidl  33429  qsidomlem2  33431  mxidlprm  33448  opprmxidlabs  33465  qsdrngilem  33472  qsdrngi  33473  qsdrnglem2  33474  idlsrg0g  33484  pidufd  33521  dfufd2lem  33527  fply1  33534  evl1fpws  33540  ressply1evls1  33541  ressply1sub  33546  ply1asclunit  33550  r1plmhm  33582  drgextlsp  33596  matdim  33618  ply1degltdimlem  33625  lindsunlem  33627  qusdimsum  33631  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdg1id  33668  evls1fldgencl  33672  irngss  33689  irngnzply1  33693  minplymindeg  33705  minplyirredlem  33707  irredminply  33713  algextdeglem2  33715  constrconj  33742  constrfiss  33748  1smat1  33801  submat1n  33802  lmatfval  33811  lmatcl  33813  mdetpmtr1  33820  madjusmdetlem4  33827  qtopt1  33832  qtophaus  33833  locfinref  33838  zarcls1  33866  zarclsiin  33868  zarmxt1  33877  zarcmplem  33878  rhmpreimacn  33882  ordtrest2NEWlem  33919  elzrhunit  33974  qqhcn  33988  qqhucn  33989  esumel  34044  esumsplit  34050  sigagenss2  34147  elsx  34191  sxbrsigalem0  34269  dya2icoseg  34275  eulerpartlemb  34366  eulerpartlemgvv  34374  iwrdsplit  34385  sseqfv2  34392  probfinmeasb  34426  dstrvprob  34470  dstfrvel  34472  ballotlemrv  34518  signstfvn  34567  signstfvp  34569  signstfveq0  34575  signsvtp  34581  signsvtn  34582  reprsuc  34613  reprpmtf1o  34624  lpadleft  34681  bnj1006  34957  bnj1018g  34960  bnj1018  34961  bnj1121  34982  bnj1398  35031  bnj1450  35047  bnj1501  35064  revpfxsfxrev  35110  swrdrevpfx  35111  pfxwlk  35118  revwlk  35119  swrdwlk  35121  subfacp1lem5  35178  ptpconn  35227  indispconn  35228  cvxsconn  35237  cvmseu  35270  cvmliftmolem2  35276  cvmliftlem7  35285  cvmliftlem10  35288  cvmliftlem13  35290  cvmlift2lem12  35308  satfv1lem  35356  satffunlem1lem2  35397  satffunlem2lem2  35400  satefvfmla1  35419  mrsubcv  35504  mrsubff  35506  mrsubrn  35507  mrsubccat  35512  elmrsubrn  35514  mrsubco  35515  mrsubvrs  35516  mvhf  35552  msubvrs  35554  mclsax  35563  r1peuqusdeg1  35637  linerflx1  36144  linerflx2  36146  fwddifnval  36158  elhf2  36170  neibastop2lem  36355  weiunpo  36460  weiunso  36461  icoreunrn  37354  relowlssretop  37358  sucneqond  37360  matunitlindflem2  37618  poimirlem4  37625  poimirlem20  37641  poimirlem30  37651  broucube  37655  opnmbllem0  37657  areacirclem2  37710  areacirclem4  37712  blssp  37757  sstotbnd2  37775  totbndbnd  37790  prdstotbnd  37795  cnpwstotbnd  37798  heiborlem9  37820  exidcl  37877  exidresid  37880  grpokerinj  37894  iscringd  37999  erimeq2  38677  prter3  38882  toycom  38973  islfld  39062  lshpsmreu  39109  ldualelvbase  39127  ldualssvscl  39158  lkreqN  39170  lkrlspeqN  39171  erng1lem  40988  erngdvlem4  40992  erng0g  40995  erng1r  40996  erngdvlem4-rN  41000  dva0g  41028  dia1dim2  41063  dia1dimid  41064  dia2dimlem5  41069  dvhelvbasei  41089  dvhvaddass  41098  tendoinvcl  41105  tendolinv  41106  tendorinv  41107  dvhgrp  41108  dvhlveclem  41109  cdlemn4  41199  lcfrlem12N  41555  lcfrlem15  41558  lcdvscl  41606  lcdlssvscl  41607  lcdvsass  41608  lcdvs0N  41617  mapdincl  41662  mapdin  41663  mapdlsmcl  41664  mapdcnvatN  41667  mapdpglem2  41674  mapdpglem12  41684  mapdpglem18  41690  mapdpglem21  41693  mapdpglem22  41694  mapdpglem28  41702  mapdpglem30  41703  hdmaprnlem3N  41851  hdmaprnlem3uN  41852  hdmaprnlem7N  41856  hdmaprnlem8N  41857  hdmaprnlem9N  41858  hdmaprnlem3eN  41859  hdmaprnlem16N  41863  hgmapdcl  41891  hgmapval1  41894  hgmaprnlem4N  41900  hdmapinvlem1  41919  fzadd2d  41973  aks6d1c2lem4  42122  sticksstones1  42141  sticksstones8  42148  sticksstones9  42149  sticksstones10  42150  sticksstones11  42151  sticksstones17  42158  sticksstones18  42159  aks6d1c6lem4  42168  rhmqusspan  42180  aks5lem2  42182  mhmcopsr  42544  evlsbagval  42561  evlsevl  42566  evlvvval  42568  evlvvvallem  42569  selvcllem2  42573  evlselv  42582  mhpind  42589  fltnltalem  42657  wepwsolem  43038  kercvrlsm  43079  dfacbasgrp  43104  onexomgt  43237  onexoegt  43240  onov0suclim  43270  cantnftermord  43316  cantnf2  43321  omcl2  43329  ofoaf  43351  ofoafo  43352  grurankcld  44229  grumnudlem  44281  grumnud  44282  inaex  44293  gruex  44294  dvconstbi  44330  cncmpmax  45033  iooabslt  45504  fmul01lt1lem2  45590  limciccioolb  45626  limcicciooub  45642  limsuppnfdlem  45706  climrescn  45753  climxrrelem  45754  climxrre  45755  liminflimsupxrre  45822  xlimmnfvlem2  45838  xlimpnfvlem2  45842  fsumcncf  45883  ioccncflimc  45890  icocncflimc  45894  cncfiooicclem1  45898  dvbdfbdioolem2  45934  dvnmul  45948  dvnprodlem1  45951  stoweidlem26  46031  stoweidlem34  46039  stoweidlem48  46053  stoweidlem59  46064  dirkercncflem3  46110  fourierdlem32  46144  fourierdlem41  46153  fourierdlem51  46162  fourierdlem63  46174  fourierdlem82  46193  fourierdlem85  46196  fourierdlem93  46204  fourierdlem111  46222  fourierdlem114  46225  etransclem35  46274  hspdifhsp  46621  opnvonmbllem1  46637  ovnovollem1  46661  mbfresmf  46744  smfaddlem1  46768  smfsuplem1  46816  smflimsuplem5  46829  setsidel  47381  setsnidel  47382  imasetpreimafvbijlemf  47406  prelspr  47491  upgrimpths  47913  gpgprismgr4cycllem9  48097  rngccatidALTV  48264  rhmsubcALTVlem3  48275  funcringcsetcALTV2lem3  48284  funcringcsetcALTV2lem8  48289  ringccatidALTV  48298  funcringcsetclem3ALTV  48307  funcringcsetclem8ALTV  48312  srhmsubcALTVlem1  48315  srhmsubcALTV  48317  lcosslsp  48431  nnolog2flm1  48583  ffvbr  48848  glbprlem  48957  topdlat  48996  catprs  49004  iinfsubc  49051  iinfconstbaslem  49058  imaid  49147  fthcomf  49150  uptr2  49214  natoppf2  49223  natoppfb  49224  swapf2  49267  swapfiso  49278  swapciso  49279  oppc1stflem  49280  cofuswapf2  49288  fuco22natlem  49338  fucoppcffth  49404  oppcthinco  49432  oppcthinendcALT  49434  thinccisod  49447  termco  49474  termchommo  49478  termcid  49479  termcterm  49506  termcterm2  49507  diagciso  49532  diagcic  49533  funcsn  49534  uobeqterm  49539  mndtccatid  49580  grptcmon  49586  grptcepi  49587  2arwcat  49593  lanval2  49620  ranval2  49623  lanup  49634  ranup  49635  lmddu  49660