Theorem eleqtrrd 2844

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

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  3eltr4d  2856  rspc2vd  3881  disjxiun  5072  eldmressnsn  5983  fnsnbg  7112  elimdelov  7456  elovmpt3rab1  7620  fnwelem  8075  tfrlem13  8323  tz7.44-2  8340  omordi  8495  oneo  8510  omeulem2  8512  oeordi  8517  oeeui  8532  nnneo  8585  naddelim  8616  erref  8658  en1uniel  8970  omxpenlem  9010  unblem3  9198  dffi3  9338  ordtypelem10  9436  oismo  9449  cantnff  9590  cantnfp1lem3  9596  cantnflem1  9605  cnfcom  9616  r1ordg  9697  r1pwss  9703  rankwflemb  9712  r1elwf  9715  rankidb  9719  rankonidlem  9747  fseqenlem2  9942  dfac12lem1  10061  dfac12lem2  10062  pwsdompw  10120  ackbij2lem3  10157  ackbij2  10159  cfsmolem  10187  hsmexlem4  10346  ttukeylem3  10428  ttukeylem7  10432  iundom2g  10457  fpwwe2lem8  10556  canthwelem  10568  pwfseqlem4  10580  winalim2  10614  r1wunlim  10655  tskmid  10758  fzopth  13510  predfz  13602  fzoss2  13637  fz1fzo0m1  13660  fzo0addel  13668  fzo0addelr  13669  elfzoext  13672  fzosubel3  13676  elfzomin  13687  elfzonlteqm1  13691  fzoend  13707  fzoopth  13712  fzofzp1  13714  fzofzp1b  13715  peano2fzor  13725  zmodfzo  13848  seqf1olem2  13999  bcn2  14276  swrdccat2  14627  pfxccat1  14659  swrdswrd  14662  pfxccatin12  14690  splfv1  14712  revcl  14718  revlen  14719  revccat  14723  revrev  14724  repswpfx  14742  cshwidxmod  14760  revco  14791  limsupgre  15438  summolem2a  15672  fsumm1  15708  fsumcom2  15731  prodmolem2a  15894  fprodm1  15927  fprodcom2  15944  prmreclem4  16885  prmreclem5  16886  vdwapid1  16941  vdwlem5  16951  vdwlem8  16954  vdwnnlem2  16962  ramub1lem1  16992  ramub1lem2  16993  mrieqvlemd  17590  mreexd  17603  mreexexlemd  17605  catcocl  17646  catass  17647  moni  17698  epii  17705  inviso1  17728  episect  17747  invisoinvl  17752  catsubcat  17801  subccocl  17807  fullsubc  17812  funcco  17833  resf2nd  17857  funcres  17858  fthepi  17892  nati  17920  arwhoma  18007  catccatid  18068  resscatc  18071  catcisolem  18072  catcoppccl  18079  catcfuccl  18080  estrreslem2  18099  funcestrcsetclem3  18103  funcestrcsetclem8  18108  equivestrcsetc  18113  funcsetcestrclem3  18117  funcsetcestrclem8  18123  xpcco  18144  xpcco2  18148  xpccatid  18149  prfcl  18164  catcxpccl  18168  curf12  18188  curf1cl  18189  curf2  18190  curf2cl  18192  curfcl  18193  uncf2  18198  uncfcurf  18200  diag12  18205  diag2  18206  curf2ndf  18208  hofcl  18220  oppchofcl  18221  oyoncl  18231  yonedalem3a  18235  yonedalem4b  18237  yonedalem22  18239  yonedalem3b  18240  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  latcl2  18397  latlem  18398  latjcom  18408  latmcom  18424  clatlem  18463  clatlubcl2  18465  clatglbcl2  18467  acsfiindd  18514  pfxchn  18571  chnind  18582  chnub  18583  chnlt  18584  chnccat  18587  chnrev  18588  gsumpropd2lem  18642  sgrppropd  18694  mndpropd  18722  imasmnd  18738  frmdmnd  18822  frmdgsum  18825  grpsubpropd2  19017  imasgrp  19027  subg0  19103  0ghm  19200  resghm2  19203  ghmco  19206  pwsdiagghm  19214  ghmqusnsglem2  19251  ghmqusnsg  19252  ghmquskerlem2  19255  ghmquskerlem3  19256  ghmqusker  19257  psgnunilem1  19463  psgnunilem5  19464  psgnunilem2  19465  psgnunilem3  19466  sylow1lem4  19571  sylow1lem5  19572  efglem  19686  efgtf  19692  efginvrel2  19697  efginvrel1  19698  efgsdmi  19702  efgs1b  19706  efgsres  19708  efgsfo  19709  efgredleme  19713  efgredlemc  19715  efgredlem  19717  efgcpbllemb  19725  frgp0  19730  frgpadd  19733  frgpinv  19734  vrgpf  19738  vrgpinv  19739  frgpuplem  19742  frgpup1  19745  frgpup2  19746  frgpup3lem  19747  frgpnabllem1  19843  frgpnabllem2  19844  gsumval3  19877  dprdfid  19989  dprdsn  20008  dprd2da  20014  dpjidcl  20030  pgpfac1lem2  20047  pgpfaclem3  20055  ablsimpg1gend  20077  ablsimpgprmd  20087  rngpropd  20150  imasrng  20153  ringpropd  20264  imasring  20305  qusring2  20309  pwsco1rhm  20477  pwsco2rhm  20478  lringuplu  20520  subrgunit  20566  pwsdiagrhm  20583  rnghmsubcsetclem1  20607  zrinitorngc  20618  zrtermorngc  20619  zrzeroorngc  20620  rhmsubcsetclem1  20636  rhmsubcrngclem1  20642  zrtermoringc  20651  zrninitoringc  20652  srhmsubclem2  20654  srhmsubc  20656  cntzsdrg  20778  isabvd  20788  lmodprop2d  20918  islssd  20929  prdsvscacl  20962  prdslmodd  20963  islmhm2  21032  lmhmco  21037  lmhmplusg  21038  lmhmvsca  21039  lmhmpropd  21067  lsppreli  21084  ellspsn4  21121  lssacsex  21141  lspsnat  21142  lidlnsg  21245  qus2idrng  21270  qus1  21271  qusrhm  21273  rhmpreimaidl  21274  rhmqusnsg  21282  rngqiprngghmlem1  21284  rngqiprngfulem1  21308  irinitoringc  21458  nzerooringczr  21459  znf1o  21530  cssmre  21672  dsmmlss  21723  frlmsplit2  21752  frlmbas3  21755  frlmup1  21777  assapropd  21850  psr0cl  21931  psrnegcl  21933  psr1cl  21939  resspsrmul  21954  subrgpsr  21956  mvrf  21963  mplmon  22015  mplcoe1  22017  subrgasclcl  22047  mplind  22050  evlslem1  22062  mhmcompl  22101  evlsevl  22112  evlvvval  22113  selvcllem2  22115  subrgply1  22221  psrplusgpropd  22224  ply1coe  22288  cply1coe0bi  22292  lply1binomsc  22301  ply1fermltlchr  22302  evls1val  22310  evls1rhm  22312  evl1val  22319  evl1rhm  22322  pf1ind  22345  evl1scvarpw  22353  evls1fpws  22359  rhmply1  22373  matbas2i  22409  matplusg2  22414  matvsca2  22415  matsubgcell  22421  matvscacell  22423  mpomatmul  22433  mavmulval  22532  mavmulcl  22534  mavmulass  22536  mavmul0  22539  mavmumamul1  22542  m1detdiag  22584  cramerimplem2  22671  mat2pmatmul  22718  mat2pmatlin  22722  monmatcollpw  22766  pmatcollpwfi  22769  mply1topmatcl  22792  pm2mpghm  22803  pm2mpmhmlem2  22806  pm2mp  22812  chpmat1dlem  22822  chpmat1d  22823  chpdmatlem0  22824  chpscmat  22829  chpscmatgsumbin  22831  chpscmatgsummon  22832  chfacfscmulcl  22844  cpmadugsumlemB  22861  cpmadugsumlemC  22862  chcoeffeqlem  22872  cldmreon  23081  neiptopreu  23120  maxlp  23134  ordttopon  23180  ordtrest2lem  23190  cnprcl2  23238  lmcnp  23291  resthauslem  23350  hauscmplem  23393  1stcfb  23432  2ndcctbss  23442  2ndcomap  23445  dis2ndc  23447  loclly  23474  hausllycmp  23481  locfincmp  23513  dissnref  23515  kgeni  23524  kgenidm  23534  ptpjpre2  23567  xkoopn  23576  txopn  23589  ptpjopn  23599  ptcldmpt  23601  ptcls  23603  pthaus  23625  txkgen  23639  xkohaus  23640  xkopt  23642  txconn  23676  imastps  23708  kqid  23715  kqopn  23721  kqcld  23722  isr0  23724  indishmph  23785  pt1hmeo  23793  ptuncnv  23794  ptunhmeo  23795  t0kq  23805  filconn  23870  uzrest  23884  uffixsn  23912  fmfnfmlem2  23942  flimss2  23959  flimss1  23960  flimclslem  23971  flfcnp  23991  fclsfnflim  24014  uffclsflim  24018  fcfelbas  24023  alexsublem  24031  alexsub  24032  cnextcn  24054  cnextfres1  24055  cnextfres  24056  tmdgsum  24082  distgp  24086  indistgp  24087  symgtgp  24093  ghmcnp  24102  qustgpopn  24107  qustgplem  24108  qustgphaus  24110  prdstmdd  24111  prdstgpd  24112  tsmsid  24127  tsmssubm  24130  tsmsmhm  24133  tsmsadd  24134  tsmssplit  24139  utop2nei  24237  utop3cls  24238  neipcfilu  24282  cnextucn  24289  ucnextcn  24290  blpnfctr  24423  lpbl  24490  met2ndci  24509  tmsxps  24523  metcnpi  24531  metcnpi2  24532  metcnpi3  24533  metustid  24541  metustsym  24542  metustexhalf  24543  subgngp  24622  ngptgp  24623  sranlm  24671  nlmvscn  24674  nrginvrcn  24679  lssnlm  24688  nghmcn  24732  iccntr  24809  icccmplem2  24811  msdcn  24829  cncfmptc  24901  cncfmptid  24902  cncfmpt2f  24904  icoopnst  24928  iocopnst  24929  nmoleub2lem3  25104  nmoleub3  25108  nmhmcn  25109  ipcn  25235  cfilfcls  25263  caucfil  25272  equivcau  25289  caubl  25297  flimcfil  25303  cmssmscld  25339  rrxdstprj1  25398  minveclem3b  25417  minveclem4  25421  mulcncf  25435  ovolicc2lem3  25508  ovolicc2lem4  25509  opnmbllem  25590  vitalilem2  25598  mbfsup  25653  mbfinf  25654  mbfi1fseqlem4  25707  limccnp  25880  limccnp2  25881  dvreslem  25898  dvres2lem  25899  dvidlem  25904  dvcnp2  25909  dvcn  25910  dvaddbr  25927  dvmulbr  25928  dvcmul  25933  dvcof  25937  dvcnvlem  25965  dvef  25969  rollelem  25978  dvlip2  25984  dvivthlem1  25997  dvivth  25999  lhop2  26004  lhop  26005  dvcnvrelem1  26006  dvcnvrelem2  26007  dvcnvre  26008  ply1rem  26153  fta1blem  26158  plycpn  26277  plyrem  26293  tayl0  26349  dvtaylp  26357  dvntaylp  26358  dvntaylp0  26359  taylthlem1  26360  taylthlem2  26361  ulmdvlem3  26389  psercn  26413  pserdv  26416  abelth  26428  efabl  26536  efopnlem1  26642  loglesqrt  26747  relogbf  26777  efrlim  26955  dchrghm  27241  dchrptlem3  27251  nodenselem5  27674  nosupres  27693  noinfres  27708  ltslpss  27922  precsexlem11  28231  noseq0  28304  noseqp1  28305  noseqrdgfn  28320  noseqrdgsuc  28322  tgbtwntriv2  28577  tgbtwnne  28580  ercgrg  28607  tgidinside  28661  tgbtwnconn1  28665  tglnne  28718  tglnne0  28730  tglnpt2  28731  tglineneq  28734  ncolncol  28736  coltr3  28738  mirln  28766  mirln2  28767  mirconn  28768  krippenlem  28780  footexALT  28808  footexlem1  28809  footexlem2  28810  colperpexlem3  28822  mideulem2  28824  opphllem  28825  oppne3  28833  opphllem1  28837  opphllem2  28838  opphllem4  28840  oppperpex  28843  opphl  28844  hlpasch  28846  hpgerlem  28855  colhp  28860  midbtwn  28869  lmieu  28874  lmiisolem  28886  sacgr  28921  f1otrg  28961  f1otrge  28962  ebtwntg  29073  ecgrtg  29074  eengtrkg  29077  eengtrkge  29078  upgr1eop  29206  usgredg3  29307  uspgr1eop  29338  usgr1eop  29341  vtxdun  29572  vtxdfiun  29573  1loopgruspgr  29591  1loopgrvd2  29594  1hevtxdg1  29597  1egrvtxdg1  29600  1egrvtxdg0  29602  umgr2v2e  29616  wlkres  29759  wlkp1lem4  29765  wlkp1  29770  cyclnumvtx  29890  wwlksm1edg  29971  wwlksnext  29983  wwlksnextproplem3  30001  clwwlkel  30138  1wlkdlem2  30230  trlsegvdeg  30319  eupth2lem3lem1  30320  eupth2lem3lem2  30321  extwwlkfab  30444  numclwlk2lem2f  30469  spansnid  31656  elspansn4  31666  fnpreimac  32766  ccatf1  33032  ccatws1f1olast  33035  swrdrn2  33037  swrdrn3  33038  swrdf1  33039  splfv3  33041  pwrssmgc  33083  suppgsumssiun  33157  wrdpmtrlast  33178  psgnfzto1stlem  33185  cycpmfv1  33198  cycpmfv2  33199  cycpmco2lem2  33212  cycpmco2lem4  33214  cycpmco2lem5  33215  cycpmco2lem6  33216  cycpmco2  33218  cyc3co2  33225  cycpmrn  33228  submarchi  33271  subrdom  33370  fracfld  33396  imaslmod  33440  quslmod  33445  quslmhm  33446  nsgqusf1olem2  33501  lmhmqusker  33504  rhmquskerlem  33512  idlinsubrg  33518  drngidl  33520  rhmpreimaprmidl  33538  qsidomlem2  33540  mxidlprm  33557  opprmxidlabs  33574  qsdrngilem  33581  qsdrngi  33582  qsdrnglem2  33583  idlsrg0g  33601  pidufd  33638  dfufd2lem  33644  fply1  33653  evl1fpws  33659  ressply1evls1  33660  ressply1sub  33665  ply1asclunit  33669  r1plmhm  33705  0mplrim  33710  selvascl  33713  selvply1rhmlema  33714  selvply1rhmlem1  33716  extvfvcl  33732  evlextv  33738  mplvrpmga  33741  psrmon  33745  psrmonprod  33748  mplmonprod  33750  issply  33757  esplympl  33763  esplyind  33771  drgextlsp  33790  matdim  33811  ply1degltdimlem  33818  lindsunlem  33820  qusdimsum  33824  fedgmullem1  33825  fedgmullem2  33826  fedgmul  33827  extdg1id  33862  evls1fldgencl  33866  irngss  33883  irngnzply1  33887  extdgfialglem1  33888  extdgfialglem2  33889  minplymindeg  33904  minplyirredlem  33906  irredminply  33912  algextdeglem2  33914  constrconj  33941  constrfiss  33947  1smat1  34000  submat1n  34001  lmatfval  34010  lmatcl  34012  mdetpmtr1  34019  madjusmdetlem4  34026  qtopt1  34031  qtophaus  34032  locfinref  34037  zarcls1  34065  zarclsiin  34067  zarmxt1  34076  zarcmplem  34077  rhmpreimacn  34081  ordtrest2NEWlem  34118  elzrhunit  34173  qqhcn  34187  qqhucn  34188  esumel  34243  esumsplit  34249  sigagenss2  34346  elsx  34390  sxbrsigalem0  34467  dya2icoseg  34473  eulerpartlemb  34564  eulerpartlemgvv  34572  iwrdsplit  34583  sseqfv2  34590  probfinmeasb  34624  dstrvprob  34668  dstfrvel  34670  ballotlemrv  34716  signstfvn  34765  signstfvp  34767  signstfveq0  34773  signsvtp  34779  signsvtn  34780  reprsuc  34811  reprpmtf1o  34822  morleylemrneab  34867  lpadleft  34882  bnj1006  35157  bnj1018g  35160  bnj1018  35161  bnj1121  35182  bnj1398  35231  bnj1450  35247  bnj1501  35264  revpfxsfxrev  35359  swrdrevpfx  35360  pfxwlk  35367  revwlk  35368  swrdwlk  35370  subfacp1lem5  35427  ptpconn  35476  indispconn  35477  cvxsconn  35486  cvmseu  35519  cvmliftmolem2  35525  cvmliftlem7  35534  cvmliftlem10  35537  cvmliftlem13  35539  cvmlift2lem12  35557  satfv1lem  35605  satffunlem1lem2  35646  satffunlem2lem2  35649  satefvfmla1  35668  mrsubcv  35753  mrsubff  35755  mrsubrn  35756  mrsubccat  35761  elmrsubrn  35763  mrsubco  35764  mrsubvrs  35765  mvhf  35801  msubvrs  35803  mclsax  35812  r1peuqusdeg1  35886  linerflx1  36392  linerflx2  36394  fwddifnval  36406  elhf2  36418  neibastop2lem  36603  weiunpo  36708  weiunso  36709  icoreunrn  37736  relowlssretop  37740  sucneqond  37742  matunitlindflem2  37999  poimirlem4  38006  poimirlem20  38022  poimirlem30  38032  broucube  38036  opnmbllem0  38038  areacirclem2  38091  areacirclem4  38093  blssp  38138  sstotbnd2  38156  totbndbnd  38171  prdstotbnd  38176  cnpwstotbnd  38179  heiborlem9  38201  exidcl  38258  exidresid  38261  grpokerinj  38275  iscringd  38380  erimeq2  39145  prter3  39389  toycom  39480  islfld  39569  lshpsmreu  39616  ldualelvbase  39634  ldualssvscl  39665  lkreqN  39677  lkrlspeqN  39678  erng1lem  41494  erngdvlem4  41498  erng0g  41501  erng1r  41502  erngdvlem4-rN  41506  dva0g  41534  dia1dim2  41569  dia1dimid  41570  dia2dimlem5  41575  dvhelvbasei  41595  dvhvaddass  41604  tendoinvcl  41611  tendolinv  41612  tendorinv  41613  dvhgrp  41614  dvhlveclem  41615  cdlemn4  41705  lcfrlem12N  42061  lcfrlem15  42064  lcdvscl  42112  lcdlssvscl  42113  lcdvsass  42114  lcdvs0N  42123  mapdincl  42168  mapdin  42169  mapdlsmcl  42170  mapdcnvatN  42173  mapdpglem2  42180  mapdpglem12  42190  mapdpglem18  42196  mapdpglem21  42199  mapdpglem22  42200  mapdpglem28  42208  mapdpglem30  42209  hdmaprnlem3N  42357  hdmaprnlem3uN  42358  hdmaprnlem7N  42362  hdmaprnlem8N  42363  hdmaprnlem9N  42364  hdmaprnlem3eN  42365  hdmaprnlem16N  42369  hgmapdcl  42397  hgmapval1  42400  hgmaprnlem4N  42406  hdmapinvlem1  42425  fzadd2d  42479  aks6d1c2lem4  42627  sticksstones1  42646  sticksstones8  42653  sticksstones9  42654  sticksstones10  42655  sticksstones11  42656  sticksstones17  42663  sticksstones18  42664  aks6d1c6lem4  42673  rhmqusspan  42685  aks5lem2  42687  mhmcopsr  43045  evlsbagval  43051  evlvvvallem  43052  evlselv  43054  mhpind  43059  fltnltalem  43127  wepwsolem  43502  kercvrlsm  43543  dfacbasgrp  43568  onexomgt  43701  onexoegt  43704  onov0suclim  43734  cantnftermord  43780  cantnf2  43785  omcl2  43793  ofoaf  43815  ofoafo  43816  grurankcld  44692  grumnudlem  44744  grumnud  44745  inaex  44756  gruex  44757  dvconstbi  44793  cncmpmax  45495  iooabslt  45958  fmul01lt1lem2  46044  limciccioolb  46080  limcicciooub  46094  limsuppnfdlem  46158  climrescn  46205  climxrrelem  46206  climxrre  46207  liminflimsupxrre  46274  xlimmnfvlem2  46290  xlimpnfvlem2  46294  fsumcncf  46335  ioccncflimc  46342  icocncflimc  46346  cncfiooicclem1  46350  dvbdfbdioolem2  46386  dvnmul  46400  dvnprodlem1  46403  stoweidlem26  46483  stoweidlem34  46491  stoweidlem48  46505  stoweidlem59  46516  dirkercncflem3  46562  fourierdlem32  46596  fourierdlem41  46605  fourierdlem51  46614  fourierdlem63  46626  fourierdlem82  46645  fourierdlem85  46648  fourierdlem93  46656  fourierdlem111  46674  fourierdlem114  46677  etransclem35  46726  hoicvr  47005  hspdifhsp  47073  opnvonmbllem1  47089  ovnovollem1  47113  mbfresmf  47196  smfaddlem1  47220  smfsuplem1  47268  smflimsuplem5  47281  chnerlem2  47342  setsidel  47865  setsnidel  47866  imasetpreimafvbijlemf  47890  prelspr  47975  upgrimpths  48414  gpgprismgr4cycllem9  48608  rngccatidALTV  48777  rhmsubcALTVlem3  48788  funcringcsetcALTV2lem3  48797  funcringcsetcALTV2lem8  48802  ringccatidALTV  48811  funcringcsetclem3ALTV  48820  funcringcsetclem8ALTV  48825  srhmsubcALTVlem1  48828  srhmsubcALTV  48830  lcosslsp  48943  nnolog2flm1  49095  ffvbr  49360  glbprlem  49469  topdlat  49508  catprs  49515  iinfsubc  49562  iinfconstbaslem  49569  imaid  49658  fthcomf  49661  uptr2  49725  natoppf2  49734  natoppfb  49735  swapf2  49778  swapfiso  49789  swapciso  49790  oppc1stflem  49791  cofuswapf2  49799  fuco22natlem  49849  fucoppcffth  49915  oppcthinco  49943  oppcthinendcALT  49945  thinccisod  49958  termco  49985  termchommo  49989  termcid  49990  termcterm  50017  termcterm2  50018  diagciso  50043  diagcic  50044  funcsn  50045  uobeqterm  50050  mndtccatid  50091  grptcmon  50097  grptcepi  50098  2arwcat  50104  lanval2  50131  ranval2  50134  lanup  50145  ranup  50146  lmddu  50171