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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  3eltr4d  2856  rspc2vd  3947  disjxiun  5140  eldmressnsn  6042  elimdelov  7529  elovmpt3rab1  7693  fnwelem  8156  tfrlem13  8430  tz7.44-2  8447  omordi  8604  oneo  8619  omeulem2  8621  oeordi  8625  oeeui  8640  nnneo  8693  naddelim  8724  erref  8765  en1uniel  9069  omxpenlem  9113  unblem3  9330  dffi3  9471  ordtypelem10  9567  oismo  9580  cantnff  9714  cantnfp1lem3  9720  cantnflem1  9729  cnfcom  9740  r1ordg  9818  r1pwss  9824  rankwflemb  9833  r1elwf  9836  rankidb  9840  rankonidlem  9868  fseqenlem2  10065  dfac12lem1  10184  dfac12lem2  10185  pwsdompw  10243  ackbij2lem3  10280  ackbij2  10282  cfsmolem  10310  hsmexlem4  10469  ttukeylem3  10551  ttukeylem7  10555  iundom2g  10580  fpwwe2lem8  10678  canthwelem  10690  pwfseqlem4  10702  winalim2  10736  r1wunlim  10777  tskmid  10880  fzopth  13601  predfz  13693  fzoss2  13727  fz1fzo0m1  13750  fzo0addel  13757  fzo0addelr  13758  elfzoext  13761  fzosubel3  13765  elfzomin  13776  elfzonlteqm1  13780  fzoend  13796  fzoopth  13801  fzofzp1  13803  fzofzp1b  13804  peano2fzor  13813  zmodfzo  13934  seqf1olem2  14083  bcn2  14358  swrdccat2  14707  pfxccat1  14740  swrdswrd  14743  pfxccatin12  14771  splfv1  14793  revcl  14799  revlen  14800  revccat  14804  revrev  14805  repswpfx  14823  cshwidxmod  14841  revco  14873  limsupgre  15517  summolem2a  15751  fsumm1  15787  fsumcom2  15810  prodmolem2a  15970  fprodm1  16003  fprodcom2  16020  prmreclem4  16957  prmreclem5  16958  vdwapid1  17013  vdwlem5  17023  vdwlem8  17026  vdwnnlem2  17034  ramub1lem1  17064  ramub1lem2  17065  mrieqvlemd  17672  mreexd  17685  mreexexlemd  17687  catcocl  17728  catass  17729  moni  17780  epii  17787  inviso1  17810  episect  17829  invisoinvl  17834  catsubcat  17884  subccocl  17890  fullsubc  17895  funcco  17916  resf2nd  17940  funcres  17941  fthepi  17975  nati  18003  arwhoma  18090  catccatid  18151  resscatc  18154  catcisolem  18155  catcoppccl  18162  catcfuccl  18163  estrreslem2  18183  funcestrcsetclem3  18187  funcestrcsetclem8  18192  equivestrcsetc  18197  funcsetcestrclem3  18201  funcsetcestrclem8  18207  xpcco  18228  xpcco2  18232  xpccatid  18233  prfcl  18248  catcxpccl  18252  curf12  18272  curf1cl  18273  curf2  18274  curf2cl  18276  curfcl  18277  uncf2  18282  uncfcurf  18284  diag12  18289  diag2  18290  curf2ndf  18292  hofcl  18304  oppchofcl  18305  oyoncl  18315  yonedalem3a  18319  yonedalem4b  18321  yonedalem22  18323  yonedalem3b  18324  yonedalem3  18325  yonedainv  18326  yonffthlem  18327  latcl2  18481  latlem  18482  latjcom  18492  latmcom  18508  clatlem  18547  clatlubcl2  18549  clatglbcl2  18551  acsfiindd  18598  gsumpropd2lem  18692  sgrppropd  18744  mndpropd  18772  imasmnd  18788  frmdmnd  18872  frmdgsum  18875  grpsubpropd2  19064  imasgrp  19074  subg0  19150  0ghm  19248  resghm2  19251  ghmco  19254  pwsdiagghm  19262  ghmqusnsglem2  19299  ghmqusnsg  19300  ghmquskerlem2  19303  ghmquskerlem3  19304  ghmqusker  19305  psgnunilem1  19511  psgnunilem5  19512  psgnunilem2  19513  psgnunilem3  19514  sylow1lem4  19619  sylow1lem5  19620  efglem  19734  efgtf  19740  efginvrel2  19745  efginvrel1  19746  efgsdmi  19750  efgs1b  19754  efgsres  19756  efgsfo  19757  efgredleme  19761  efgredlemc  19763  efgredlem  19765  efgcpbllemb  19773  frgp0  19778  frgpadd  19781  frgpinv  19782  vrgpf  19786  vrgpinv  19787  frgpuplem  19790  frgpup1  19793  frgpup2  19794  frgpup3lem  19795  frgpnabllem1  19891  frgpnabllem2  19892  gsumval3  19925  dprdfid  20037  dprdsn  20056  dprd2da  20062  dpjidcl  20078  pgpfac1lem2  20095  pgpfaclem3  20103  ablsimpg1gend  20125  ablsimpgprmd  20135  rngpropd  20171  imasrng  20174  ringpropd  20285  imasring  20327  qusring2  20331  pwsco1rhm  20502  pwsco2rhm  20503  lringuplu  20544  subrgunit  20590  pwsdiagrhm  20607  rnghmsubcsetclem1  20631  zrinitorngc  20642  zrtermorngc  20643  zrzeroorngc  20644  rhmsubcsetclem1  20660  rhmsubcrngclem1  20666  zrtermoringc  20675  zrninitoringc  20676  srhmsubclem2  20678  srhmsubc  20680  cntzsdrg  20803  isabvd  20813  lmodprop2d  20922  islssd  20933  prdsvscacl  20966  prdslmodd  20967  islmhm2  21037  lmhmco  21042  lmhmplusg  21043  lmhmvsca  21044  lmhmpropd  21072  lsppreli  21089  ellspsn4  21126  lssacsex  21146  lspsnat  21147  lidlnsg  21258  qus2idrng  21283  qus1  21284  qusrhm  21286  rhmpreimaidl  21287  rhmqusnsg  21295  rngqiprngghmlem1  21297  rngqiprngfulem1  21321  irinitoringc  21490  nzerooringczr  21491  znf1o  21570  cssmre  21711  dsmmlss  21764  frlmsplit2  21793  frlmbas3  21796  frlmup1  21818  assapropd  21892  psr0cl  21972  psrnegcl  21974  psr1cl  21981  resspsrmul  21996  subrgpsr  21998  mvrf  22005  mplmon  22053  mplcoe1  22055  subrgasclcl  22091  mplind  22094  evlslem1  22106  subrgply1  22234  psrplusgpropd  22237  ply1coe  22302  cply1coe0bi  22306  lply1binomsc  22315  ply1fermltlchr  22316  evls1val  22324  evls1rhm  22326  evl1val  22333  evl1rhm  22336  pf1ind  22359  evl1scvarpw  22367  evls1fpws  22373  mhmcompl  22384  rhmply1  22390  matbas2i  22428  matplusg2  22433  matvsca2  22434  matsubgcell  22440  matvscacell  22442  mpomatmul  22452  mavmulval  22551  mavmulcl  22553  mavmulass  22555  mavmul0  22558  mavmumamul1  22561  m1detdiag  22603  cramerimplem2  22690  mat2pmatmul  22737  mat2pmatlin  22741  monmatcollpw  22785  pmatcollpwfi  22788  mply1topmatcl  22811  pm2mpghm  22822  pm2mpmhmlem2  22825  pm2mp  22831  chpmat1dlem  22841  chpmat1d  22842  chpdmatlem0  22843  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  chfacfscmulcl  22863  cpmadugsumlemB  22880  cpmadugsumlemC  22881  chcoeffeqlem  22891  cldmreon  23102  neiptopreu  23141  maxlp  23155  ordttopon  23201  ordtrest2lem  23211  cnprcl2  23259  lmcnp  23312  resthauslem  23371  hauscmplem  23414  1stcfb  23453  2ndcctbss  23463  2ndcomap  23466  dis2ndc  23468  loclly  23495  hausllycmp  23502  locfincmp  23534  dissnref  23536  kgeni  23545  kgenidm  23555  ptpjpre2  23588  xkoopn  23597  txopn  23610  ptpjopn  23620  ptcldmpt  23622  ptcls  23624  pthaus  23646  txkgen  23660  xkohaus  23661  xkopt  23663  txconn  23697  imastps  23729  kqid  23736  kqopn  23742  kqcld  23743  isr0  23745  indishmph  23806  pt1hmeo  23814  ptuncnv  23815  ptunhmeo  23816  t0kq  23826  filconn  23891  uzrest  23905  uffixsn  23933  fmfnfmlem2  23963  flimss2  23980  flimss1  23981  flimclslem  23992  flfcnp  24012  fclsfnflim  24035  uffclsflim  24039  fcfelbas  24044  alexsublem  24052  alexsub  24053  cnextcn  24075  cnextfres1  24076  cnextfres  24077  tmdgsum  24103  distgp  24107  indistgp  24108  symgtgp  24114  ghmcnp  24123  qustgpopn  24128  qustgplem  24129  qustgphaus  24131  prdstmdd  24132  prdstgpd  24133  tsmsid  24148  tsmssubm  24151  tsmsmhm  24154  tsmsadd  24155  tsmssplit  24160  utop2nei  24259  utop3cls  24260  neipcfilu  24305  cnextucn  24312  ucnextcn  24313  blpnfctr  24446  lpbl  24516  met2ndci  24535  tmsxps  24549  metcnpi  24557  metcnpi2  24558  metcnpi3  24559  metustid  24567  metustsym  24568  metustexhalf  24569  subgngp  24648  ngptgp  24649  sranlm  24705  nlmvscn  24708  nrginvrcn  24713  lssnlm  24722  nghmcn  24766  iccntr  24843  icccmplem2  24845  msdcn  24863  cncfmptc  24938  cncfmptid  24939  cncfmpt2f  24941  icoopnst  24969  iocopnst  24970  nmoleub2lem3  25148  nmoleub3  25152  nmhmcn  25153  ipcn  25280  cfilfcls  25308  caucfil  25317  equivcau  25334  caubl  25342  flimcfil  25348  cmssmscld  25384  rrxdstprj1  25443  minveclem3b  25462  minveclem4  25466  mulcncf  25480  ovolicc2lem3  25554  ovolicc2lem4  25555  opnmbllem  25636  vitalilem2  25644  mbfsup  25699  mbfinf  25700  mbfi1fseqlem4  25753  limccnp  25926  limccnp2  25927  dvreslem  25944  dvres2lem  25945  dvidlem  25950  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmul  25981  dvcof  25986  dvcnvlem  26014  dvef  26018  rollelem  26027  dvlip2  26034  dvivthlem1  26047  dvivth  26049  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  ply1rem  26205  fta1blem  26210  plycpn  26331  plyrem  26347  tayl0  26403  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem3  26445  psercn  26470  pserdv  26473  abelth  26485  efabl  26592  efopnlem1  26698  loglesqrt  26804  relogbf  26834  efrlim  27012  efrlimOLD  27013  dchrghm  27300  dchrptlem3  27310  nodenselem5  27733  nosupres  27752  noinfres  27767  sltlpss  27945  precsexlem11  28241  noseq0  28296  noseqp1  28297  noseqrdgfn  28312  noseqrdgsuc  28314  tgbtwntriv2  28495  tgbtwnne  28498  ercgrg  28525  tgidinside  28579  tgbtwnconn1  28583  tglnne  28636  tglnne0  28648  tglnpt2  28649  tglineneq  28652  ncolncol  28654  coltr3  28656  mirln  28684  mirln2  28685  mirconn  28686  krippenlem  28698  footexALT  28726  footexlem1  28727  footexlem2  28728  colperpexlem3  28740  mideulem2  28742  opphllem  28743  oppne3  28751  opphllem1  28755  opphllem2  28756  opphllem4  28758  oppperpex  28761  opphl  28762  hlpasch  28764  hpgerlem  28773  colhp  28778  midbtwn  28787  lmieu  28792  lmiisolem  28804  sacgr  28839  f1otrg  28879  f1otrge  28880  ebtwntg  28997  ecgrtg  28998  eengtrkg  29001  eengtrkge  29002  upgr1eop  29132  usgredg3  29233  uspgr1eop  29264  usgr1eop  29267  vtxdun  29499  vtxdfiun  29500  1loopgruspgr  29518  1loopgrvd2  29521  1hevtxdg1  29524  1egrvtxdg1  29527  1egrvtxdg0  29529  umgr2v2e  29543  wlkres  29688  wlkp1lem4  29694  wlkp1  29699  cyclnumvtx  29820  wwlksm1edg  29901  wwlksnext  29913  wwlksnextproplem3  29931  clwwlkel  30065  1wlkdlem2  30157  trlsegvdeg  30246  eupth2lem3lem1  30247  eupth2lem3lem2  30248  extwwlkfab  30371  numclwlk2lem2f  30396  spansnid  31582  elspansn4  31592  fnpreimac  32681  ccatf1  32933  ccatws1f1olast  32937  swrdrn2  32939  swrdrn3  32940  swrdf1  32941  splfv3  32943  pwrssmgc  32990  pfxchn  32999  chnind  33001  chnub  33002  chnlt  33003  wrdpmtrlast  33113  psgnfzto1stlem  33120  cycpmfv1  33133  cycpmfv2  33134  cycpmco2lem2  33147  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  cyc3co2  33160  cycpmrn  33163  submarchi  33193  subrdom  33288  fracfld  33310  imaslmod  33381  quslmod  33386  quslmhm  33387  nsgqusf1olem2  33442  lmhmqusker  33445  rhmquskerlem  33453  idlinsubrg  33459  drngidl  33461  rhmpreimaprmidl  33479  qsidomlem2  33481  mxidlprm  33498  opprmxidlabs  33515  qsdrngilem  33522  qsdrngi  33523  qsdrnglem2  33524  idlsrg0g  33534  pidufd  33571  dfufd2lem  33577  fply1  33584  evl1fpws  33590  ressply1sub  33595  ply1asclunit  33599  r1plmhm  33630  drgextlsp  33644  matdim  33666  ply1degltdimlem  33673  lindsunlem  33675  qusdimsum  33679  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  extdg1id  33716  evls1fldgencl  33720  irngss  33737  irngnzply1  33741  minplymindeg  33751  minplyirredlem  33753  irredminply  33757  algextdeglem2  33759  constrconj  33786  1smat1  33803  submat1n  33804  lmatfval  33813  lmatcl  33815  mdetpmtr1  33822  madjusmdetlem4  33829  qtopt1  33834  qtophaus  33835  locfinref  33840  zarcls1  33868  zarclsiin  33870  zarmxt1  33879  zarcmplem  33880  rhmpreimacn  33884  ordtrest2NEWlem  33921  elzrhunit  33978  qqhcn  33992  qqhucn  33993  esumel  34048  esumsplit  34054  sigagenss2  34151  elsx  34195  sxbrsigalem0  34273  dya2icoseg  34279  eulerpartlemb  34370  eulerpartlemgvv  34378  iwrdsplit  34389  sseqfv2  34396  probfinmeasb  34430  dstrvprob  34474  dstfrvel  34476  ballotlemrv  34522  signstfvn  34584  signstfvp  34586  signstfveq0  34592  signsvtp  34598  signsvtn  34599  reprsuc  34630  reprpmtf1o  34641  lpadleft  34698  bnj1006  34974  bnj1018g  34977  bnj1018  34978  bnj1121  34999  bnj1398  35048  bnj1450  35064  bnj1501  35081  revpfxsfxrev  35121  swrdrevpfx  35122  pfxwlk  35129  revwlk  35130  swrdwlk  35132  subfacp1lem5  35189  ptpconn  35238  indispconn  35239  cvxsconn  35248  cvmseu  35281  cvmliftmolem2  35287  cvmliftlem7  35296  cvmliftlem10  35299  cvmliftlem13  35301  cvmlift2lem12  35319  satfv1lem  35367  satffunlem1lem2  35408  satffunlem2lem2  35411  satefvfmla1  35430  mrsubcv  35515  mrsubff  35517  mrsubrn  35518  mrsubccat  35523  elmrsubrn  35525  mrsubco  35526  mrsubvrs  35527  mvhf  35563  msubvrs  35565  mclsax  35574  r1peuqusdeg1  35648  linerflx1  36150  linerflx2  36152  fwddifnval  36164  elhf2  36176  neibastop2lem  36361  weiunpo  36466  weiunso  36467  icoreunrn  37360  relowlssretop  37364  sucneqond  37366  matunitlindflem2  37624  poimirlem4  37631  poimirlem20  37647  poimirlem30  37657  broucube  37661  opnmbllem0  37663  areacirclem2  37716  areacirclem4  37718  blssp  37763  sstotbnd2  37781  totbndbnd  37796  prdstotbnd  37801  cnpwstotbnd  37804  heiborlem9  37826  exidcl  37883  exidresid  37886  grpokerinj  37900  iscringd  38005  erimeq2  38679  prter3  38883  toycom  38974  islfld  39063  lshpsmreu  39110  ldualelvbase  39128  ldualssvscl  39159  lkreqN  39171  lkrlspeqN  39172  erng1lem  40989  erngdvlem4  40993  erng0g  40996  erng1r  40997  erngdvlem4-rN  41001  dva0g  41029  dia1dim2  41064  dia1dimid  41065  dia2dimlem5  41070  dvhelvbasei  41090  dvhvaddass  41099  tendoinvcl  41106  tendolinv  41107  tendorinv  41108  dvhgrp  41109  dvhlveclem  41110  cdlemn4  41200  lcfrlem12N  41556  lcfrlem15  41559  lcdvscl  41607  lcdlssvscl  41608  lcdvsass  41609  lcdvs0N  41618  mapdincl  41663  mapdin  41664  mapdlsmcl  41665  mapdcnvatN  41668  mapdpglem2  41675  mapdpglem12  41685  mapdpglem18  41691  mapdpglem21  41694  mapdpglem22  41695  mapdpglem28  41703  mapdpglem30  41704  hdmaprnlem3N  41852  hdmaprnlem3uN  41853  hdmaprnlem7N  41857  hdmaprnlem8N  41858  hdmaprnlem9N  41859  hdmaprnlem3eN  41860  hdmaprnlem16N  41864  hgmapdcl  41892  hgmapval1  41895  hgmaprnlem4N  41901  hdmapinvlem1  41920  fzadd2d  41979  aks6d1c2lem4  42128  sticksstones1  42147  sticksstones8  42154  sticksstones9  42155  sticksstones10  42156  sticksstones11  42157  sticksstones17  42164  sticksstones18  42165  aks6d1c6lem4  42174  rhmqusspan  42186  aks5lem2  42188  fnsnbt  42271  mhmcopsr  42559  evlsbagval  42576  evlsevl  42581  evlvvval  42583  evlvvvallem  42584  selvcllem2  42588  evlselv  42597  mhpind  42604  fltnltalem  42672  wepwsolem  43054  kercvrlsm  43095  dfacbasgrp  43120  onexomgt  43253  onexoegt  43256  onov0suclim  43287  cantnftermord  43333  cantnf2  43338  omcl2  43346  ofoaf  43368  ofoafo  43369  grurankcld  44252  grumnudlem  44304  grumnud  44305  inaex  44316  gruex  44317  dvconstbi  44353  cncmpmax  45037  iooabslt  45512  fmul01lt1lem2  45600  limciccioolb  45636  limcicciooub  45652  limsuppnfdlem  45716  climrescn  45763  climxrrelem  45764  climxrre  45765  liminflimsupxrre  45832  xlimmnfvlem2  45848  xlimpnfvlem2  45852  fsumcncf  45893  ioccncflimc  45900  icocncflimc  45904  cncfiooicclem1  45908  dvbdfbdioolem2  45944  dvnmul  45958  dvnprodlem1  45961  stoweidlem26  46041  stoweidlem34  46049  stoweidlem48  46063  stoweidlem59  46074  dirkercncflem3  46120  fourierdlem32  46154  fourierdlem41  46163  fourierdlem51  46172  fourierdlem63  46184  fourierdlem82  46203  fourierdlem85  46206  fourierdlem93  46214  fourierdlem111  46232  fourierdlem114  46235  etransclem35  46284  hspdifhsp  46631  opnvonmbllem1  46647  ovnovollem1  46671  mbfresmf  46754  smfaddlem1  46778  smfsuplem1  46826  smflimsuplem5  46839  setsidel  47363  setsnidel  47364  imasetpreimafvbijlemf  47388  prelspr  47473  rngccatidALTV  48188  rhmsubcALTVlem3  48199  funcringcsetcALTV2lem3  48208  funcringcsetcALTV2lem8  48213  ringccatidALTV  48222  funcringcsetclem3ALTV  48231  funcringcsetclem8ALTV  48236  srhmsubcALTVlem1  48239  srhmsubcALTV  48241  lcosslsp  48355  nnolog2flm1  48511  glbprlem  48862  topdlat  48893  catprs  48900  swapf2  48980  swapfiso  48991  swapciso  48992  cofuswapf2  48995  fuco22natlem  49040  oppcthinco  49088  oppcthinendcALT  49090  thinccisod  49103  termchommo  49130  termcid  49131  termcterm  49145  termcterm2  49146  mndtccatid  49184  grptcmon  49190  grptcepi  49191