Theorem eleqtrrd 2835

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr4d  2847  rspc2vd  3909  disjxiun  5107  eldmressnsn  5985  elimdelov  7458  elovmpt3rab1  7618  fnwelem  8068  tfrlem13  8341  tz7.44-2  8358  omordi  8518  oneo  8533  omeulem2  8535  oeordi  8539  oeeui  8554  nnneo  8606  naddelim  8637  erref  8675  en1uniel  8979  en1unielOLD  8980  omxpenlem  9024  unblem3  9248  dffi3  9376  ordtypelem10  9472  oismo  9485  cantnff  9619  cantnfp1lem3  9625  cantnflem1  9634  cnfcom  9645  r1ordg  9723  r1pwss  9729  rankwflemb  9738  r1elwf  9741  rankidb  9745  rankonidlem  9773  fseqenlem2  9970  dfac12lem1  10088  dfac12lem2  10089  pwsdompw  10149  ackbij2lem3  10186  ackbij2  10188  cfsmolem  10215  hsmexlem4  10374  ttukeylem3  10456  ttukeylem7  10460  iundom2g  10485  fpwwe2lem8  10583  canthwelem  10595  pwfseqlem4  10607  winalim2  10641  r1wunlim  10682  tskmid  10785  fzopth  13488  predfz  13576  fzoss2  13610  fz1fzo0m1  13630  fzo0addel  13636  fzo0addelr  13637  fzosubel3  13643  elfzomin  13654  elfzonlteqm1  13658  fzoend  13673  fzofzp1  13679  fzofzp1b  13680  peano2fzor  13689  zmodfzo  13809  seqf1olem2  13958  bcn2  14229  swrdccat2  14569  pfxccat1  14602  swrdswrd  14605  pfxccatin12  14633  splfv1  14655  revcl  14661  revlen  14662  revccat  14666  revrev  14667  repswpfx  14685  cshwidxmod  14703  revco  14735  limsupgre  15375  summolem2a  15611  fsumm1  15647  fsumcom2  15670  prodmolem2a  15828  fprodm1  15861  fprodcom2  15878  prmreclem4  16802  prmreclem5  16803  vdwapid1  16858  vdwlem5  16868  vdwlem8  16871  vdwnnlem2  16879  ramub1lem1  16909  ramub1lem2  16910  mrieqvlemd  17523  mreexd  17536  mreexexlemd  17538  catcocl  17579  catass  17580  moni  17633  epii  17640  inviso1  17663  episect  17682  invisoinvl  17687  catsubcat  17739  subccocl  17745  fullsubc  17750  funcco  17771  resf2nd  17795  funcres  17796  fthepi  17829  nati  17856  arwhoma  17945  catccatid  18006  resscatc  18009  catcisolem  18010  catcoppccl  18017  catcoppcclOLD  18018  catcfuccl  18019  catcfucclOLD  18020  estrreslem2  18040  funcestrcsetclem3  18044  funcestrcsetclem8  18049  equivestrcsetc  18054  funcsetcestrclem3  18058  funcsetcestrclem8  18064  xpcco  18085  xpcco2  18089  xpccatid  18090  prfcl  18105  catcxpccl  18109  catcxpcclOLD  18110  curf12  18130  curf1cl  18131  curf2  18132  curf2cl  18134  curfcl  18135  uncf2  18140  uncfcurf  18142  diag12  18147  diag2  18148  curf2ndf  18150  hofcl  18162  oppchofcl  18163  oyoncl  18173  yonedalem3a  18177  yonedalem4b  18179  yonedalem22  18181  yonedalem3b  18182  yonedalem3  18183  yonedainv  18184  yonffthlem  18185  latcl2  18339  latlem  18340  latjcom  18350  latmcom  18366  clatlem  18405  clatlubcl2  18407  clatglbcl2  18409  acsfiindd  18456  gsumpropd2lem  18548  mndpropd  18595  imasmnd  18608  frmdmnd  18683  frmdgsum  18686  grpsubpropd2  18867  imasgrp  18877  subg0  18948  0ghm  19036  resghm2  19039  ghmco  19042  pwsdiagghm  19050  psgnunilem1  19289  psgnunilem5  19290  psgnunilem2  19291  psgnunilem3  19292  sylow1lem4  19397  sylow1lem5  19398  efglem  19512  efgtf  19518  efginvrel2  19523  efginvrel1  19524  efgsdmi  19528  efgs1b  19532  efgsres  19534  efgsfo  19535  efgredleme  19539  efgredlemc  19541  efgredlem  19543  efgcpbllemb  19551  frgp0  19556  frgpadd  19559  frgpinv  19560  vrgpf  19564  vrgpinv  19565  frgpuplem  19568  frgpup1  19571  frgpup2  19572  frgpup3lem  19573  frgpnabllem1  19665  frgpnabllem2  19666  gsumval3  19698  dprdfid  19810  dprdsn  19829  dprd2da  19835  dpjidcl  19851  pgpfac1lem2  19868  pgpfaclem3  19876  ablsimpg1gend  19898  ablsimpgprmd  19908  ringpropd  20020  imasring  20059  qusring2  20060  pwsco1rhm  20188  pwsco2rhm  20189  lringuplu  20224  subrgunit  20288  pwsdiagrhm  20306  cntzsdrg  20325  isabvd  20335  lmodprop2d  20441  islssd  20453  prdsvscacl  20486  prdslmodd  20487  islmhm2  20556  lmhmco  20561  lmhmplusg  20562  lmhmvsca  20563  lmhmpropd  20591  lsppreli  20608  lspsnel4  20644  lssacsex  20664  lspsnat  20665  qus1  20764  qusrhm  20766  znf1o  20995  cssmre  21134  dsmmlss  21187  frlmsplit2  21216  frlmbas3  21219  frlmup1  21241  assapropd  21312  psr0cl  21399  psrnegcl  21401  psr1cl  21408  resspsrmul  21423  subrgpsr  21425  mvrf  21430  mplmon  21473  mplcoe1  21475  subrgasclcl  21512  mplind  21515  evlslem1  21529  subrgply1  21641  psrplusgpropd  21644  ply1coe  21704  cply1coe0bi  21708  lply1binomsc  21715  evls1val  21723  evls1rhm  21725  evl1val  21732  evl1rhm  21735  pf1ind  21758  evl1scvarpw  21766  matbas2i  21808  matplusg2  21813  matvsca2  21814  matsubgcell  21820  matvscacell  21822  mpomatmul  21832  mavmulval  21931  mavmulcl  21933  mavmulass  21935  mavmul0  21938  mavmumamul1  21941  m1detdiag  21983  cramerimplem2  22070  mat2pmatmul  22117  mat2pmatlin  22121  monmatcollpw  22165  pmatcollpwfi  22168  mply1topmatcl  22191  pm2mpghm  22202  pm2mpmhmlem2  22205  pm2mp  22211  chpmat1dlem  22221  chpmat1d  22222  chpdmatlem0  22223  chpscmat  22228  chpscmatgsumbin  22230  chpscmatgsummon  22231  chfacfscmulcl  22243  cpmadugsumlemB  22260  cpmadugsumlemC  22261  chcoeffeqlem  22271  cldmreon  22482  neiptopreu  22521  maxlp  22535  ordttopon  22581  ordtrest2lem  22591  cnprcl2  22639  lmcnp  22692  resthauslem  22751  hauscmplem  22794  1stcfb  22833  2ndcctbss  22843  2ndcomap  22846  dis2ndc  22848  loclly  22875  hausllycmp  22882  locfincmp  22914  dissnref  22916  kgeni  22925  kgenidm  22935  ptpjpre2  22968  xkoopn  22977  txopn  22990  ptpjopn  23000  ptcldmpt  23002  ptcls  23004  pthaus  23026  txkgen  23040  xkohaus  23041  xkopt  23043  txconn  23077  imastps  23109  kqid  23116  kqopn  23122  kqcld  23123  isr0  23125  indishmph  23186  pt1hmeo  23194  ptuncnv  23195  ptunhmeo  23196  t0kq  23206  filconn  23271  uzrest  23285  uffixsn  23313  fmfnfmlem2  23343  flimss2  23360  flimss1  23361  flimclslem  23372  flfcnp  23392  fclsfnflim  23415  uffclsflim  23419  fcfelbas  23424  alexsublem  23432  alexsub  23433  cnextcn  23455  cnextfres1  23456  cnextfres  23457  tmdgsum  23483  distgp  23487  indistgp  23488  symgtgp  23494  ghmcnp  23503  qustgpopn  23508  qustgplem  23509  qustgphaus  23511  prdstmdd  23512  prdstgpd  23513  tsmsid  23528  tsmssubm  23531  tsmsmhm  23534  tsmsadd  23535  tsmssplit  23540  utop2nei  23639  utop3cls  23640  neipcfilu  23685  cnextucn  23692  ucnextcn  23693  blpnfctr  23826  lpbl  23896  met2ndci  23915  tmsxps  23929  metcnpi  23937  metcnpi2  23938  metcnpi3  23939  metustid  23947  metustsym  23948  metustexhalf  23949  subgngp  24028  ngptgp  24029  sranlm  24085  nlmvscn  24088  nrginvrcn  24093  lssnlm  24102  nghmcn  24146  iccntr  24221  icccmplem2  24223  msdcn  24241  cncfmptc  24312  cncfmptid  24313  cncfmpt2f  24315  icoopnst  24339  iocopnst  24340  nmoleub2lem3  24515  nmoleub3  24519  nmhmcn  24520  ipcn  24647  cfilfcls  24675  caucfil  24684  equivcau  24701  caubl  24709  flimcfil  24715  cmssmscld  24751  rrxdstprj1  24810  minveclem3b  24829  minveclem4  24833  ovolicc2lem3  24920  ovolicc2lem4  24921  opnmbllem  25002  vitalilem2  25010  mbfsup  25065  mbfinf  25066  mbfi1fseqlem4  25120  limccnp  25292  limccnp2  25293  dvreslem  25310  dvres2lem  25311  dvidlem  25316  dvcnp2  25321  dvcn  25322  dvaddbr  25339  dvmulbr  25340  dvcmul  25345  dvcof  25349  dvcnvlem  25377  dvef  25381  rollelem  25390  dvlip2  25396  dvivthlem1  25409  dvivth  25411  lhop2  25416  lhop  25417  dvcnvrelem1  25418  dvcnvrelem2  25419  dvcnvre  25420  ply1rem  25565  fta1blem  25570  plycpn  25686  plyrem  25702  tayl0  25758  dvtaylp  25766  dvntaylp  25767  dvntaylp0  25768  taylthlem1  25769  taylthlem2  25770  ulmdvlem3  25798  psercn  25822  pserdv  25825  abelth  25837  efabl  25943  efopnlem1  26048  loglesqrt  26148  relogbf  26178  efrlim  26356  dchrghm  26641  dchrptlem3  26651  nodenselem5  27073  nosupres  27092  noinfres  27107  sltlpss  27279  tgbtwntriv2  27492  tgbtwnne  27495  ercgrg  27522  tgidinside  27576  tgbtwnconn1  27580  tglnne  27633  tglnne0  27645  tglnpt2  27646  tglineneq  27649  ncolncol  27651  coltr3  27653  mirln  27681  mirln2  27682  mirconn  27683  krippenlem  27695  footexALT  27723  footexlem1  27724  footexlem2  27725  colperpexlem3  27737  mideulem2  27739  opphllem  27740  oppne3  27748  opphllem1  27752  opphllem2  27753  opphllem4  27755  oppperpex  27758  opphl  27759  hlpasch  27761  hpgerlem  27770  colhp  27775  midbtwn  27784  lmieu  27789  lmiisolem  27801  sacgr  27836  f1otrg  27876  f1otrge  27877  ebtwntg  27994  ecgrtg  27995  eengtrkg  27998  eengtrkge  27999  upgr1eop  28129  usgredg3  28227  uspgr1eop  28258  usgr1eop  28261  vtxdun  28492  vtxdfiun  28493  1loopgruspgr  28511  1loopgrvd2  28514  1hevtxdg1  28517  1egrvtxdg1  28520  1egrvtxdg0  28522  umgr2v2e  28536  wlkres  28681  wlkp1lem4  28687  wlkp1  28692  wwlksm1edg  28889  wwlksnext  28901  wwlksnextproplem3  28919  clwwlkel  29053  1wlkdlem2  29145  trlsegvdeg  29234  eupth2lem3lem1  29235  eupth2lem3lem2  29236  extwwlkfab  29359  numclwlk2lem2f  29384  spansnid  30568  elspansn4  30578  fnpreimac  31654  ccatf1  31875  swrdrn2  31878  swrdrn3  31879  swrdf1  31880  splfv3  31882  pwrssmgc  31930  psgnfzto1stlem  32019  cycpmfv1  32032  cycpmfv2  32033  cycpmco2lem2  32046  cycpmco2lem4  32048  cycpmco2lem5  32049  cycpmco2lem6  32050  cycpmco2  32052  cyc3co2  32059  cycpmrn  32062  submarchi  32092  imaslmod  32216  quslmod  32217  quslmhm  32218  nsgqusf1olem2  32266  ghmquskerlem2  32271  ghmqusker  32272  lmhmqusker  32273  rhmpreimaidl  32275  rhmqusker  32278  idlinsubrg  32281  lidlnsg  32294  rhmpreimaprmidl  32300  qsidomlem2  32302  mxidlprm  32313  idlsrg0g  32324  fply1  32341  evls1fpws  32348  ressply1sub  32358  ply1fermltlchr  32361  drgextlsp  32379  matdim  32397  ply1degltdimlem  32404  lindsunlem  32406  qusdimsum  32410  fedgmullem1  32411  fedgmullem2  32412  fedgmul  32413  extdg1id  32439  irngss  32448  irngnzply1  32452  1smat1  32474  submat1n  32475  lmatfval  32484  lmatcl  32486  mdetpmtr1  32493  madjusmdetlem4  32500  qtopt1  32505  qtophaus  32506  locfinref  32511  zarcls1  32539  zarclsiin  32541  zarmxt1  32550  zarcmplem  32551  rhmpreimacn  32555  ordtrest2NEWlem  32592  elzrhunit  32649  qqhcn  32661  qqhucn  32662  esumel  32735  esumsplit  32741  sigagenss2  32838  elsx  32882  sxbrsigalem0  32960  dya2icoseg  32966  eulerpartlemb  33057  eulerpartlemgvv  33065  iwrdsplit  33076  sseqfv2  33083  probfinmeasb  33117  dstrvprob  33160  dstfrvel  33162  ballotlemrv  33208  signstfvn  33270  signstfvp  33272  signstfveq0  33278  signsvtp  33284  signsvtn  33285  reprsuc  33317  reprpmtf1o  33328  lpadleft  33385  bnj1006  33661  bnj1018g  33664  bnj1018  33665  bnj1121  33686  bnj1398  33735  bnj1450  33751  bnj1501  33768  revpfxsfxrev  33796  swrdrevpfx  33797  pfxwlk  33804  revwlk  33805  swrdwlk  33807  subfacp1lem5  33865  ptpconn  33914  indispconn  33915  cvxsconn  33924  cvmseu  33957  cvmliftmolem2  33963  cvmliftlem7  33972  cvmliftlem10  33975  cvmliftlem13  33977  cvmlift2lem12  33995  satfv1lem  34043  satffunlem1lem2  34084  satffunlem2lem2  34087  satefvfmla1  34106  mrsubcv  34191  mrsubff  34193  mrsubrn  34194  mrsubccat  34199  elmrsubrn  34201  mrsubco  34202  mrsubvrs  34203  mvhf  34239  msubvrs  34241  mclsax  34250  linerflx1  34810  linerflx2  34812  fwddifnval  34824  elhf2  34836  neibastop2lem  34908  icoreunrn  35903  relowlssretop  35907  sucneqond  35909  matunitlindflem2  36148  poimirlem4  36155  poimirlem20  36171  poimirlem30  36181  broucube  36185  opnmbllem0  36187  areacirclem2  36240  areacirclem4  36242  blssp  36288  sstotbnd2  36306  totbndbnd  36321  prdstotbnd  36326  cnpwstotbnd  36329  heiborlem9  36351  exidcl  36408  exidresid  36411  grpokerinj  36425  iscringd  36530  erimeq2  37213  prter3  37417  toycom  37508  islfld  37597  lshpsmreu  37644  ldualelvbase  37662  ldualssvscl  37693  lkreqN  37705  lkrlspeqN  37706  erng1lem  39523  erngdvlem4  39527  erng0g  39530  erng1r  39531  erngdvlem4-rN  39535  dva0g  39563  dia1dim2  39598  dia1dimid  39599  dia2dimlem5  39604  dvhelvbasei  39624  dvhvaddass  39633  tendoinvcl  39640  tendolinv  39641  tendorinv  39642  dvhgrp  39643  dvhlveclem  39644  cdlemn4  39734  lcfrlem12N  40090  lcfrlem15  40093  lcdvscl  40141  lcdlssvscl  40142  lcdvsass  40143  lcdvs0N  40152  mapdincl  40197  mapdin  40198  mapdlsmcl  40199  mapdcnvatN  40202  mapdpglem2  40209  mapdpglem12  40219  mapdpglem18  40225  mapdpglem21  40228  mapdpglem22  40229  mapdpglem28  40237  mapdpglem30  40238  hdmaprnlem3N  40386  hdmaprnlem3uN  40387  hdmaprnlem7N  40391  hdmaprnlem8N  40392  hdmaprnlem9N  40393  hdmaprnlem3eN  40394  hdmaprnlem16N  40398  hgmapdcl  40426  hgmapval1  40429  hgmaprnlem4N  40435  hdmapinvlem1  40454  fzadd2d  40508  sticksstones1  40627  sticksstones8  40634  sticksstones9  40635  sticksstones10  40636  sticksstones11  40637  sticksstones17  40644  sticksstones18  40645  fnsnbt  40728  mhmcompl  40794  evlsbagval  40806  evlsevl  40810  selvcllem2  40814  mhpind  40827  mhphf  40829  fltnltalem  41058  wepwsolem  41427  kercvrlsm  41468  dfacbasgrp  41493  onexomgt  41633  onexoegt  41636  onov0suclim  41667  cantnftermord  41713  cantnf2  41718  omcl2  41726  ofoaf  41748  ofoafo  41749  imo72b2lem0  42560  grurankcld  42635  grumnudlem  42687  grumnud  42688  inaex  42699  gruex  42700  dvconstbi  42736  cncmpmax  43359  iooabslt  43857  fmul01lt1lem2  43946  limciccioolb  43982  limcicciooub  43998  limsuppnfdlem  44062  climrescn  44109  climxrrelem  44110  climxrre  44111  liminflimsupxrre  44178  xlimmnfvlem2  44194  xlimpnfvlem2  44198  fsumcncf  44239  ioccncflimc  44246  icocncflimc  44250  cncfiooicclem1  44254  dvbdfbdioolem2  44290  dvnmul  44304  stoweidlem26  44387  stoweidlem34  44395  stoweidlem48  44409  stoweidlem59  44420  dirkercncflem3  44466  fourierdlem32  44500  fourierdlem41  44509  fourierdlem51  44518  fourierdlem63  44530  fourierdlem82  44549  fourierdlem85  44552  fourierdlem93  44560  fourierdlem111  44578  fourierdlem114  44581  etransclem35  44630  hspdifhsp  44977  opnvonmbllem1  44993  ovnovollem1  45017  mbfresmf  45100  smfaddlem1  45124  smfsuplem1  45172  smflimsuplem5  45185  fzoopth  45679  setsidel  45688  setsnidel  45689  imasetpreimafvbijlemf  45713  prelspr  45798  rnghmsubcsetclem1  46393  rngccatidALTV  46407  zrinitorngc  46418  zrtermorngc  46419  zrzeroorngc  46420  rhmsubcsetclem1  46439  rhmsubcrngclem1  46445  funcringcsetcALTV2lem3  46456  funcringcsetcALTV2lem8  46461  ringccatidALTV  46470  funcringcsetclem3ALTV  46479  funcringcsetclem8ALTV  46484  irinitoringc  46487  zrtermoringc  46488  zrninitoringc  46489  nzerooringczr  46490  srhmsubclem2  46492  srhmsubc  46494  srhmsubcALTVlem1  46510  srhmsubcALTV  46512  rhmsubcALTVlem3  46524  lcosslsp  46639  nnolog2flm1  46796  glbprlem  47118  topdlat  47149  catprs  47151  mndtccatid  47233  grptcmon  47236  grptcepi  47237