Theorem eleqtrrd 2867

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 2770	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2866	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  3eltr4d  2879  rspc2vd  3902  disjxiun  5099  eldmressnsn  6012  fnsnbg  7150  elimdelov  7494  elovmpt3rab1  7658  fnwelem  8113  tfrlem13  8363  tz7.44-2  8380  omordi  8537  oneo  8552  omeulem2  8554  oeordi  8559  oeeui  8574  nnneo  8627  naddelim  8659  erref  8701  en1uniel  9012  omxpenlem  9052  unblem3  9240  dffi3  9379  ordtypelem10  9477  oismo  9490  cantnff  9631  cantnfp1lem3  9637  cantnflem1  9646  cnfcom  9657  r1ordg  9738  r1pwss  9744  rankwflemb  9753  r1elwf  9756  rankidb  9760  rankonidlem  9788  fseqenlem2  9983  dfac12lem1  10102  dfac12lem2  10103  pwsdompw  10161  ackbij2lem3  10198  ackbij2  10200  cfsmolem  10229  hsmexlem4  10388  ttukeylem3  10470  ttukeylem7  10474  iundom2g  10499  fpwwe2lem8  10598  canthwelem  10610  pwfseqlem4  10622  winalim2  10656  r1wunlim  10697  tskmid  10800  fzopth  13568  predfz  13660  fzoss2  13695  fz1fzo0m1  13718  fzo0addel  13726  fzo0addelr  13727  elfzoext  13730  fzosubel3  13734  elfzomin  13745  elfzonlteqm1  13749  fzoend  13765  fzoopth  13770  fzofzp1  13772  fzofzp1b  13773  peano2fzor  13783  zmodfzo  13906  seqf1olem2  14057  bcn2  14334  swrdccat2  14685  pfxccat1  14717  swrdswrd  14720  pfxccatin12  14748  splfv1  14770  revcl  14776  revlen  14777  revccat  14781  revrev  14782  repswpfx  14800  cshwidxmod  14818  revco  14849  limsupgre  15510  summolem2a  15744  fsumm1  15780  fsumcom2  15803  prodmolem2a  15966  fprodm1  15999  fprodcom2  16016  prmreclem4  16957  prmreclem5  16958  vdwapid1  17013  vdwlem5  17023  vdwlem8  17026  vdwnnlem2  17034  ramub1lem1  17064  ramub1lem2  17065  mrieqvlemd  17663  mreexd  17676  mreexexlemd  17678  catcocl  17719  catass  17720  moni  17771  epii  17778  inviso1  17801  episect  17820  invisoinvl  17825  catsubcat  17874  subccocl  17880  fullsubc  17885  funcco  17906  resf2nd  17930  funcres  17931  fthepi  17965  nati  17993  arwhoma  18080  catccatid  18141  resscatc  18144  catcisolem  18145  catcoppccl  18152  catcfuccl  18153  estrreslem2  18172  funcestrcsetclem3  18176  funcestrcsetclem8  18181  equivestrcsetc  18186  funcsetcestrclem3  18190  funcsetcestrclem8  18196  xpcco  18217  xpcco2  18221  xpccatid  18222  prfcl  18237  catcxpccl  18241  curf12  18261  curf1cl  18262  curf2  18263  curf2cl  18265  curfcl  18266  uncf2  18271  uncfcurf  18273  diag12  18278  diag2  18279  curf2ndf  18281  hofcl  18293  oppchofcl  18294  oyoncl  18304  yonedalem3a  18308  yonedalem4b  18310  yonedalem22  18312  yonedalem3b  18313  yonedalem3  18314  yonedainv  18315  yonffthlem  18316  latcl2  18470  latlem  18471  latjcom  18481  latmcom  18497  clatlem  18536  clatlubcl2  18538  clatglbcl2  18540  acsfiindd  18587  pfxchn  18644  chnind  18655  chnub  18656  chnlt  18657  chnccat  18660  chnrev  18661  gsumpropd2lem  18715  sgrppropd  18767  mndpropd  18795  imasmnd  18811  frmdmnd  18895  frmdgsum  18898  grpsubpropd2  19090  imasgrp  19100  subg0  19176  0ghm  19272  resghm2  19275  ghmco  19278  pwsdiagghm  19286  ghmqusnsglem2  19323  ghmqusnsg  19324  ghmquskerlem2  19327  ghmquskerlem3  19328  ghmqusker  19329  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  sylow1lem4  19643  sylow1lem5  19644  efglem  19758  efgtf  19764  efginvrel2  19769  efginvrel1  19770  efgsdmi  19774  efgs1b  19778  efgsres  19780  efgsfo  19781  efgredleme  19785  efgredlemc  19787  efgredlem  19789  efgcpbllemb  19797  frgp0  19802  frgpadd  19805  frgpinv  19806  vrgpf  19810  vrgpinv  19811  frgpuplem  19814  frgpup1  19817  frgpup2  19818  frgpup3lem  19819  frgpnabllem1  19915  frgpnabllem2  19916  gsumval3  19949  dprdfid  20061  dprdsn  20080  dprd2da  20086  dpjidcl  20102  pgpfac1lem2  20119  pgpfaclem3  20127  ablsimpg1gend  20149  ablsimpgprmd  20159  rngpropd  20222  imasrng  20225  ringpropd  20340  imasring  20381  qusring2  20385  pwsco1rhm  20553  pwsco2rhm  20554  lringuplu  20596  subrgunit  20642  pwsdiagrhm  20659  rnghmsubcsetclem1  20683  zrinitorngc  20694  zrtermorngc  20695  zrzeroorngc  20696  rhmsubcsetclem1  20712  rhmsubcrngclem1  20718  zrtermoringc  20727  zrninitoringc  20728  srhmsubclem2  20730  srhmsubc  20732  cntzsdrg  20853  isabvd  20863  lmodprop2d  20993  islssd  21004  prdsvscacl  21037  prdslmodd  21038  islmhm2  21107  lmhmco  21112  lmhmplusg  21113  lmhmvsca  21114  lmhmpropd  21142  lsppreli  21159  ellspsn4  21196  lssacsex  21216  lspsnat  21217  lidlnsg  21320  qus2idrng  21345  qus1  21346  qusrhm  21348  rhmpreimaidl  21349  rhmqusnsg  21357  rngqiprngghmlem1  21359  rngqiprngfulem1  21383  irinitoringc  21533  nzerooringczr  21534  znf1o  21605  cssmre  21747  dsmmlss  21798  frlmsplit2  21827  frlmbas3  21830  frlmup1  21852  assapropd  21925  psr0cl  22006  psrnegcl  22008  psr1cl  22014  resspsrmul  22029  subrgpsr  22031  mvrf  22038  mplmon  22090  mplcoe1  22092  subrgasclcl  22122  mplind  22125  evlslem1  22137  mhmcompl  22176  evlsevl  22187  evlvvval  22188  selvcllem2  22190  subrgply1  22296  psrplusgpropd  22299  ply1coe  22363  cply1coe0bi  22367  lply1binomsc  22376  ply1fermltlchr  22377  evls1val  22385  evls1rhm  22387  evl1val  22394  evl1rhm  22397  pf1ind  22420  evl1scvarpw  22428  evls1fpws  22434  rhmply1  22448  matbas2i  22484  matplusg2  22489  matvsca2  22490  matsubgcell  22496  matvscacell  22498  mpomatmul  22508  mavmulval  22607  mavmulcl  22609  mavmulass  22611  mavmul0  22614  mavmumamul1  22617  m1detdiag  22659  cramerimplem2  22746  mat2pmatmul  22793  mat2pmatlin  22797  monmatcollpw  22841  pmatcollpwfi  22844  mply1topmatcl  22867  pm2mpghm  22878  pm2mpmhmlem2  22881  pm2mp  22887  chpmat1dlem  22897  chpmat1d  22898  chpdmatlem0  22899  chpscmat  22904  chpscmatgsumbin  22906  chpscmatgsummon  22907  chfacfscmulcl  22919  cpmadugsumlemB  22936  cpmadugsumlemC  22937  chcoeffeqlem  22947  cldmreon  23156  neiptopreu  23195  maxlp  23209  ordttopon  23255  ordtrest2lem  23265  cnprcl2  23313  lmcnp  23366  resthauslem  23425  hauscmplem  23468  1stcfb  23507  2ndcctbss  23517  2ndcomap  23520  dis2ndc  23522  loclly  23549  hausllycmp  23556  locfincmp  23588  dissnref  23590  kgeni  23599  kgenidm  23609  ptpjpre2  23642  xkoopn  23651  txopn  23664  ptpjopn  23674  ptcldmpt  23676  ptcls  23678  pthaus  23700  txkgen  23714  xkohaus  23715  xkopt  23717  txconn  23751  imastps  23783  kqid  23790  kqopn  23796  kqcld  23797  isr0  23799  indishmph  23860  pt1hmeo  23868  ptuncnv  23869  ptunhmeo  23870  t0kq  23880  filconn  23945  uzrest  23959  uffixsn  23987  fmfnfmlem2  24017  flimss2  24034  flimss1  24035  flimclslem  24046  flfcnp  24066  fclsfnflim  24089  uffclsflim  24093  fcfelbas  24098  alexsublem  24106  alexsub  24107  cnextcn  24129  cnextfres1  24130  cnextfres  24131  tmdgsum  24157  distgp  24161  indistgp  24162  symgtgp  24168  ghmcnp  24177  qustgpopn  24182  qustgplem  24183  qustgphaus  24185  prdstmdd  24186  prdstgpd  24187  tsmsid  24202  tsmssubm  24205  tsmsmhm  24208  tsmsadd  24209  tsmssplit  24214  utop2nei  24312  utop3cls  24313  neipcfilu  24357  cnextucn  24364  ucnextcn  24365  blpnfctr  24498  lpbl  24565  met2ndci  24584  tmsxps  24598  metcnpi  24606  metcnpi2  24607  metcnpi3  24608  metustid  24616  metustsym  24617  metustexhalf  24618  subgngp  24697  ngptgp  24698  sranlm  24746  nlmvscn  24749  nrginvrcn  24754  lssnlm  24763  nghmcn  24807  iccntr  24884  icccmplem2  24886  msdcn  24904  cncfmptc  24976  cncfmptid  24977  cncfmpt2f  24979  icoopnst  25003  iocopnst  25004  nmoleub2lem3  25179  nmoleub3  25183  nmhmcn  25184  ipcn  25310  cfilfcls  25338  caucfil  25347  equivcau  25364  caubl  25372  flimcfil  25378  cmssmscld  25414  rrxdstprj1  25473  minveclem3b  25492  minveclem4  25496  mulcncf  25510  ovolicc2lem3  25583  ovolicc2lem4  25584  opnmbllem  25665  vitalilem2  25673  mbfsup  25728  mbfinf  25729  mbfi1fseqlem4  25782  limccnp  25955  limccnp2  25956  dvreslem  25973  dvres2lem  25974  dvidlem  25979  dvcnp2  25984  dvcn  25985  dvaddbr  26002  dvmulbr  26003  dvcmul  26008  dvcof  26012  dvcnvlem  26040  dvef  26044  rollelem  26053  dvlip2  26059  dvivthlem1  26072  dvivth  26074  lhop2  26079  lhop  26080  dvcnvrelem1  26081  dvcnvrelem2  26082  dvcnvre  26083  ply1rem  26228  fta1blem  26233  plycpn  26355  plyrem  26371  tayl0  26427  dvtaylp  26435  dvntaylp  26436  dvntaylp0  26437  taylthlem1  26438  taylthlem2  26439  ulmdvlem3  26467  psercn  26491  pserdv  26494  abelth  26506  efabl  26617  efopnlem1  26723  loglesqrt  26828  relogbf  26858  efrlim  27036  dchrghm  27322  dchrptlem3  27332  nodenselem5  27754  nosupres  27773  noinfres  27788  ltslpss  28003  precsexlem11  28312  noseq0  28385  noseqp1  28386  noseqrdgfn  28401  noseqrdgsuc  28403  tgbtwntriv2  28658  tgbtwnne  28661  ercgrg  28688  tgidinside  28742  tgbtwnconn1  28746  tglnne  28799  tglinesseq  28811  tglnne0  28812  tglineneq  28816  ncolncol  28818  coltr3  28820  tglnpt2  28824  tglnpt3  28825  mirln  28851  mirln2  28852  mirconn  28853  krippenlem  28865  footexALT  28893  footexlem1  28894  footexlem2  28895  colperpexlem3  28907  mideulem2  28909  opphllem  28910  oppne3  28918  opphllem1  28922  opphllem2  28923  opphllem4  28925  oppperpex  28928  opphl  28929  hlpasch  28931  hpgerlem  28940  colhp  28945  midbtwn  28954  lmieu  28959  lmiisolem  28971  plngval  28986  lnincplng  28993  plngrotlem1  28996  lnssplnglem  29000  plng3p  29002  sacgr  29027  f1otrg  29073  f1otrge  29074  ebtwntg  29185  ecgrtg  29186  eengtrkg  29189  eengtrkge  29190  upgr1eop  29318  usgredg3  29419  uspgr1eop  29450  usgr1eop  29453  vtxdun  29684  vtxdfiun  29685  1loopgruspgr  29703  1loopgrvd2  29706  1hevtxdg1  29709  1egrvtxdg1  29712  1egrvtxdg0  29714  umgr2v2e  29728  wlkres  29871  wlkp1lem4  29877  wlkp1  29882  cyclnumvtx  30002  wwlksm1edg  30083  wwlksnext  30095  wwlksnextproplem3  30113  clwwlkel  30250  1wlkdlem2  30342  trlsegvdeg  30431  eupth2lem3lem1  30432  eupth2lem3lem2  30433  extwwlkfab  30556  numclwlk2lem2f  30581  spansnid  31768  elspansn4  31778  fnpreimac  32874  ccatf1  33129  ccatws1f1olast  33132  swrdrn2  33134  swrdrn3  33135  swrdf1  33136  splfv3  33138  pwrssmgc  33180  suppgsumssiun  33254  wrdpmtrlast  33275  psgnfzto1stlem  33282  cycpmfv1  33295  cycpmfv2  33296  cycpmco2lem2  33309  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cycpmco2  33315  cyc3co2  33322  cycpmrn  33325  submarchi  33368  subrdom  33471  fracfld  33497  imaslmod  33541  quslmod  33546  quslmhm  33547  nsgqusf1olem2  33602  lmhmqusker  33605  rhmquskerlem  33613  idlinsubrg  33619  drngidl  33621  rhmpreimaprmidl  33640  qsidomlem2  33642  mxidlprm  33660  opprmxidlabs  33677  qsdrngilem  33684  qsdrngi  33685  qsdrnglem2  33686  idlsrg0g  33704  pidufd  33741  dfufd2lem  33747  fply1  33756  evl1fpws  33762  ressply1evls1  33763  ressply1sub  33768  ply1asclunit  33772  r1plmhm  33808  0mplrim  33813  selvascl  33816  selvply1rhmlema  33817  selvply1rhmlem1  33819  extvfvcl  33835  evlextv  33841  mplvrpmga  33844  psrmon  33848  psrmonprod  33851  mplmonprod  33853  issply  33860  esplympl  33866  esplyind  33874  drgextlsp  33893  matdim  33914  ply1degltdimlem  33921  lindsunlem  33923  qusdimsum  33927  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  extdg1id  33965  evls1fldgencl  33969  irngss  33986  irngnzply1  33990  extdgfialglem1  33991  extdgfialglem2  33992  minplymindeg  34007  minplyirredlem  34009  irredminply  34015  algextdeglem2  34017  constrconj  34044  constrfiss  34050  1smat1  34103  submat1n  34104  lmatfval  34113  lmatcl  34115  mdetpmtr1  34122  madjusmdetlem4  34129  qtopt1  34134  qtophaus  34135  locfinref  34140  zarcls1  34168  zarclsiin  34170  zarmxt1  34179  zarcmplem  34180  rhmpreimacn  34184  ordtrest2NEWlem  34221  elzrhunit  34276  qqhcn  34290  qqhucn  34291  esumel  34346  esumsplit  34352  sigagenss2  34449  elsx  34493  sxbrsigalem0  34570  dya2icoseg  34576  eulerpartlemb  34667  eulerpartlemgvv  34675  iwrdsplit  34686  sseqfv2  34693  probfinmeasb  34727  dstrvprob  34771  dstfrvel  34773  ballotlemrv  34819  signstfvn  34865  signstfvp  34867  signstfveq0  34873  signsvtp  34879  signsvtn  34880  reprsuc  34911  reprpmtf1o  34922  morleylemrneab  34967  lpadleft  34982  bnj1006  35257  bnj1018g  35260  bnj1018  35261  bnj1121  35282  bnj1398  35331  bnj1450  35347  bnj1501  35364  revpfxsfxrev  35470  swrdrevpfx  35471  pfxwlk  35479  revwlk  35480  swrdwlk  35482  subfacp1lem5  35539  ptpconn  35588  indispconn  35589  cvxsconn  35598  cvmseu  35631  cvmliftmolem2  35637  cvmliftlem7  35646  cvmliftlem10  35649  cvmliftlem13  35651  cvmlift2lem12  35669  satfv1lem  35717  satffunlem1lem2  35758  satffunlem2lem2  35761  satefvfmla1  35780  mrsubcv  35865  mrsubff  35867  mrsubrn  35868  mrsubccat  35873  elmrsubrn  35875  mrsubco  35876  mrsubvrs  35877  mvhf  35913  msubvrs  35915  mclsax  35924  r1peuqusdeg1  35998  linerflx1  36504  linerflx2  36506  fwddifnval  36518  elhf2  36530  neibastop2lem  36725  weiunpo  36830  weiunso  36831  icoreunrn  37858  relowlssretop  37862  sucneqond  37864  matunitlindflem2  38121  poimirlem4  38128  poimirlem20  38144  poimirlem30  38154  broucube  38158  opnmbllem0  38160  areacirclem2  38213  areacirclem4  38215  blssp  38260  sstotbnd2  38278  totbndbnd  38293  prdstotbnd  38298  cnpwstotbnd  38301  heiborlem9  38323  exidcl  38380  exidresid  38383  grpokerinj  38397  iscringd  38502  erimeq2  39267  prter3  39511  toycom  39602  islfld  39691  lshpsmreu  39738  ldualelvbase  39756  ldualssvscl  39787  lkreqN  39799  lkrlspeqN  39800  erng1lem  41616  erngdvlem4  41620  erng0g  41623  erng1r  41624  erngdvlem4-rN  41628  dva0g  41656  dia1dim2  41691  dia1dimid  41692  dia2dimlem5  41697  dvhelvbasei  41717  dvhvaddass  41726  tendoinvcl  41733  tendolinv  41734  tendorinv  41735  dvhgrp  41736  dvhlveclem  41737  cdlemn4  41827  lcfrlem12N  42183  lcfrlem15  42186  lcdvscl  42234  lcdlssvscl  42235  lcdvsass  42236  lcdvs0N  42245  mapdincl  42290  mapdin  42291  mapdlsmcl  42292  mapdcnvatN  42295  mapdpglem2  42302  mapdpglem12  42312  mapdpglem18  42318  mapdpglem21  42321  mapdpglem22  42322  mapdpglem28  42330  mapdpglem30  42331  hdmaprnlem3N  42479  hdmaprnlem3uN  42480  hdmaprnlem7N  42484  hdmaprnlem8N  42485  hdmaprnlem9N  42486  hdmaprnlem3eN  42487  hdmaprnlem16N  42491  hgmapdcl  42519  hgmapval1  42522  hgmaprnlem4N  42528  hdmapinvlem1  42547  fzadd2d  42601  aks6d1c2lem4  42749  sticksstones1  42768  sticksstones8  42775  sticksstones9  42776  sticksstones10  42777  sticksstones11  42778  sticksstones17  42785  sticksstones18  42786  aks6d1c6lem4  42795  rhmqusspan  42807  aks5lem2  42809  mhmcopsr  43167  evlsbagval  43173  evlvvvallem  43174  evlselv  43176  mhpind  43181  fltnltalem  43249  wepwsolem  43624  kercvrlsm  43665  dfacbasgrp  43690  onexomgt  43823  onexoegt  43826  onov0suclim  43856  cantnftermord  43902  cantnf2  43907  omcl2  43915  ofoaf  43937  ofoafo  43938  grurankcld  44814  grumnudlem  44866  grumnud  44867  inaex  44878  gruex  44879  dvconstbi  44915  cncmpmax  45617  iooabslt  46080  fmul01lt1lem2  46166  limciccioolb  46202  limcicciooub  46216  limsuppnfdlem  46280  climrescn  46327  climxrrelem  46328  climxrre  46329  liminflimsupxrre  46396  xlimmnfvlem2  46412  xlimpnfvlem2  46416  fsumcncf  46457  ioccncflimc  46464  cncfuni  46465  icocncflimc  46468  cncfiooicclem1  46472  dvbdfbdioolem2  46508  dvnmul  46522  dvnprodlem1  46525  stoweidlem26  46605  stoweidlem34  46613  stoweidlem48  46627  stoweidlem59  46638  dirkercncflem3  46684  fourierdlem32  46718  fourierdlem41  46727  fourierdlem51  46736  fourierdlem63  46748  fourierdlem82  46767  fourierdlem85  46770  fourierdlem93  46778  fourierdlem111  46796  fourierdlem114  46799  etransclem35  46848  hoicvr  47127  hspdifhsp  47195  opnvonmbllem1  47211  ovnovollem1  47235  mbfresmf  47318  smfaddlem1  47342  smfsuplem1  47390  smflimsuplem5  47403  chnerlem2  47464  setsidel  47987  setsnidel  47988  imasetpreimafvbijlemf  48012  prelspr  48097  upgrimpths  48536  gpgprismgr4cycllem9  48730  rngccatidALTV  48899  rhmsubcALTVlem3  48910  funcringcsetcALTV2lem3  48919  funcringcsetcALTV2lem8  48924  ringccatidALTV  48933  funcringcsetclem3ALTV  48942  funcringcsetclem8ALTV  48947  srhmsubcALTVlem1  48950  srhmsubcALTV  48952  lcosslsp  49065  nnolog2flm1  49217  ffvbr  49482  glbprlem  49591  topdlat  49630  catprs  49637  iinfsubc  49684  iinfconstbaslem  49691  imaid  49780  fthcomf  49783  uptr2  49847  natoppf2  49856  natoppfb  49857  swapf2  49900  swapfiso  49911  swapciso  49912  oppc1stflem  49913  cofuswapf2  49921  fuco22natlem  49971  fucoppcffth  50037  oppcthinco  50065  oppcthinendcALT  50067  thinccisod  50080  termco  50107  termchommo  50111  termcid  50112  termcterm  50139  termcterm2  50140  diagciso  50165  diagcic  50166  funcsn  50167  uobeqterm  50172  mndtccatid  50213  grptcmon  50219  grptcepi  50220  2arwcat  50226  lanval2  50253  ranval2  50256  lanup  50267  ranup  50268  lmddu  50293