Theorem eleqtrrd 2847

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  3eltr4d  2859  rspc2vd  3972  disjxiun  5163  eldmressnsn  6053  elimdelov  7546  elovmpt3rab1  7710  fnwelem  8172  tfrlem13  8446  tz7.44-2  8463  omordi  8622  oneo  8637  omeulem2  8639  oeordi  8643  oeeui  8658  nnneo  8711  naddelim  8742  erref  8783  en1uniel  9093  en1unielOLD  9094  omxpenlem  9139  unblem3  9358  dffi3  9500  ordtypelem10  9596  oismo  9609  cantnff  9743  cantnfp1lem3  9749  cantnflem1  9758  cnfcom  9769  r1ordg  9847  r1pwss  9853  rankwflemb  9862  r1elwf  9865  rankidb  9869  rankonidlem  9897  fseqenlem2  10094  dfac12lem1  10213  dfac12lem2  10214  pwsdompw  10272  ackbij2lem3  10309  ackbij2  10311  cfsmolem  10339  hsmexlem4  10498  ttukeylem3  10580  ttukeylem7  10584  iundom2g  10609  fpwwe2lem8  10707  canthwelem  10719  pwfseqlem4  10731  winalim2  10765  r1wunlim  10806  tskmid  10909  fzopth  13621  predfz  13710  fzoss2  13744  fz1fzo0m1  13764  fzo0addel  13770  fzo0addelr  13771  fzosubel3  13777  elfzomin  13788  elfzonlteqm1  13792  fzoend  13807  fzoopth  13812  fzofzp1  13814  fzofzp1b  13815  peano2fzor  13824  zmodfzo  13945  seqf1olem2  14093  bcn2  14368  swrdccat2  14717  pfxccat1  14750  swrdswrd  14753  pfxccatin12  14781  splfv1  14803  revcl  14809  revlen  14810  revccat  14814  revrev  14815  repswpfx  14833  cshwidxmod  14851  revco  14883  limsupgre  15527  summolem2a  15763  fsumm1  15799  fsumcom2  15822  prodmolem2a  15982  fprodm1  16015  fprodcom2  16032  prmreclem4  16966  prmreclem5  16967  vdwapid1  17022  vdwlem5  17032  vdwlem8  17035  vdwnnlem2  17043  ramub1lem1  17073  ramub1lem2  17074  mrieqvlemd  17687  mreexd  17700  mreexexlemd  17702  catcocl  17743  catass  17744  moni  17797  epii  17804  inviso1  17827  episect  17846  invisoinvl  17851  catsubcat  17903  subccocl  17909  fullsubc  17914  funcco  17935  resf2nd  17959  funcres  17960  fthepi  17995  nati  18023  arwhoma  18112  catccatid  18173  resscatc  18176  catcisolem  18177  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  estrreslem2  18207  funcestrcsetclem3  18211  funcestrcsetclem8  18216  equivestrcsetc  18221  funcsetcestrclem3  18225  funcsetcestrclem8  18231  xpcco  18252  xpcco2  18256  xpccatid  18257  prfcl  18272  catcxpccl  18276  catcxpcclOLD  18277  curf12  18297  curf1cl  18298  curf2  18299  curf2cl  18301  curfcl  18302  uncf2  18307  uncfcurf  18309  diag12  18314  diag2  18315  curf2ndf  18317  hofcl  18329  oppchofcl  18330  oyoncl  18340  yonedalem3a  18344  yonedalem4b  18346  yonedalem22  18348  yonedalem3b  18349  yonedalem3  18350  yonedainv  18351  yonffthlem  18352  latcl2  18506  latlem  18507  latjcom  18517  latmcom  18533  clatlem  18572  clatlubcl2  18574  clatglbcl2  18576  acsfiindd  18623  gsumpropd2lem  18717  sgrppropd  18769  mndpropd  18797  imasmnd  18810  frmdmnd  18894  frmdgsum  18897  grpsubpropd2  19086  imasgrp  19096  subg0  19172  0ghm  19270  resghm2  19273  ghmco  19276  pwsdiagghm  19284  ghmqusnsglem2  19321  ghmqusnsg  19322  ghmquskerlem2  19325  ghmquskerlem3  19326  ghmqusker  19327  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  20201  imasrng  20204  ringpropd  20311  imasring  20353  qusring2  20357  pwsco1rhm  20528  pwsco2rhm  20529  lringuplu  20570  subrgunit  20618  pwsdiagrhm  20635  rnghmsubcsetclem1  20653  zrinitorngc  20664  zrtermorngc  20665  zrzeroorngc  20666  rhmsubcsetclem1  20682  rhmsubcrngclem1  20688  zrtermoringc  20697  zrninitoringc  20698  srhmsubclem2  20700  srhmsubc  20702  cntzsdrg  20825  isabvd  20835  lmodprop2d  20944  islssd  20956  prdsvscacl  20989  prdslmodd  20990  islmhm2  21060  lmhmco  21065  lmhmplusg  21066  lmhmvsca  21067  lmhmpropd  21095  lsppreli  21112  ellspsn4  21149  lssacsex  21169  lspsnat  21170  lidlnsg  21281  qus2idrng  21306  qus1  21307  qusrhm  21309  rhmpreimaidl  21310  rhmqusnsg  21318  rngqiprngghmlem1  21320  rngqiprngfulem1  21344  irinitoringc  21513  nzerooringczr  21514  znf1o  21593  cssmre  21734  dsmmlss  21787  frlmsplit2  21816  frlmbas3  21819  frlmup1  21841  assapropd  21915  psr0cl  21995  psrnegcl  21997  psr1cl  22004  resspsrmul  22019  subrgpsr  22021  mvrf  22028  mplmon  22076  mplcoe1  22078  subrgasclcl  22114  mplind  22117  evlslem1  22129  subrgply1  22255  psrplusgpropd  22258  ply1coe  22323  cply1coe0bi  22327  lply1binomsc  22336  ply1fermltlchr  22337  evls1val  22345  evls1rhm  22347  evl1val  22354  evl1rhm  22357  pf1ind  22380  evl1scvarpw  22388  evls1fpws  22394  mhmcompl  22405  rhmply1  22411  matbas2i  22449  matplusg2  22454  matvsca2  22455  matsubgcell  22461  matvscacell  22463  mpomatmul  22473  mavmulval  22572  mavmulcl  22574  mavmulass  22576  mavmul0  22579  mavmumamul1  22582  m1detdiag  22624  cramerimplem2  22711  mat2pmatmul  22758  mat2pmatlin  22762  monmatcollpw  22806  pmatcollpwfi  22809  mply1topmatcl  22832  pm2mpghm  22843  pm2mpmhmlem2  22846  pm2mp  22852  chpmat1dlem  22862  chpmat1d  22863  chpdmatlem0  22864  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  chfacfscmulcl  22884  cpmadugsumlemB  22901  cpmadugsumlemC  22902  chcoeffeqlem  22912  cldmreon  23123  neiptopreu  23162  maxlp  23176  ordttopon  23222  ordtrest2lem  23232  cnprcl2  23280  lmcnp  23333  resthauslem  23392  hauscmplem  23435  1stcfb  23474  2ndcctbss  23484  2ndcomap  23487  dis2ndc  23489  loclly  23516  hausllycmp  23523  locfincmp  23555  dissnref  23557  kgeni  23566  kgenidm  23576  ptpjpre2  23609  xkoopn  23618  txopn  23631  ptpjopn  23641  ptcldmpt  23643  ptcls  23645  pthaus  23667  txkgen  23681  xkohaus  23682  xkopt  23684  txconn  23718  imastps  23750  kqid  23757  kqopn  23763  kqcld  23764  isr0  23766  indishmph  23827  pt1hmeo  23835  ptuncnv  23836  ptunhmeo  23837  t0kq  23847  filconn  23912  uzrest  23926  uffixsn  23954  fmfnfmlem2  23984  flimss2  24001  flimss1  24002  flimclslem  24013  flfcnp  24033  fclsfnflim  24056  uffclsflim  24060  fcfelbas  24065  alexsublem  24073  alexsub  24074  cnextcn  24096  cnextfres1  24097  cnextfres  24098  tmdgsum  24124  distgp  24128  indistgp  24129  symgtgp  24135  ghmcnp  24144  qustgpopn  24149  qustgplem  24150  qustgphaus  24152  prdstmdd  24153  prdstgpd  24154  tsmsid  24169  tsmssubm  24172  tsmsmhm  24175  tsmsadd  24176  tsmssplit  24181  utop2nei  24280  utop3cls  24281  neipcfilu  24326  cnextucn  24333  ucnextcn  24334  blpnfctr  24467  lpbl  24537  met2ndci  24556  tmsxps  24570  metcnpi  24578  metcnpi2  24579  metcnpi3  24580  metustid  24588  metustsym  24589  metustexhalf  24590  subgngp  24669  ngptgp  24670  sranlm  24726  nlmvscn  24729  nrginvrcn  24734  lssnlm  24743  nghmcn  24787  iccntr  24862  icccmplem2  24864  msdcn  24882  cncfmptc  24957  cncfmptid  24958  cncfmpt2f  24960  icoopnst  24988  iocopnst  24989  nmoleub2lem3  25167  nmoleub3  25171  nmhmcn  25172  ipcn  25299  cfilfcls  25327  caucfil  25336  equivcau  25353  caubl  25361  flimcfil  25367  cmssmscld  25403  rrxdstprj1  25462  minveclem3b  25481  minveclem4  25485  mulcncf  25499  ovolicc2lem3  25573  ovolicc2lem4  25574  opnmbllem  25655  vitalilem2  25663  mbfsup  25718  mbfinf  25719  mbfi1fseqlem4  25773  limccnp  25946  limccnp2  25947  dvreslem  25964  dvres2lem  25965  dvidlem  25970  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmul  26001  dvcof  26006  dvcnvlem  26034  dvef  26038  rollelem  26047  dvlip2  26054  dvivthlem1  26067  dvivth  26069  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  ply1rem  26225  fta1blem  26230  plycpn  26349  plyrem  26365  tayl0  26421  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  psercn  26488  pserdv  26491  abelth  26503  efabl  26610  efopnlem1  26716  loglesqrt  26822  relogbf  26852  efrlim  27030  efrlimOLD  27031  dchrghm  27318  dchrptlem3  27328  nodenselem5  27751  nosupres  27770  noinfres  27785  sltlpss  27963  precsexlem11  28259  noseq0  28314  noseqp1  28315  noseqrdgfn  28330  noseqrdgsuc  28332  tgbtwntriv2  28513  tgbtwnne  28516  ercgrg  28543  tgidinside  28597  tgbtwnconn1  28601  tglnne  28654  tglnne0  28666  tglnpt2  28667  tglineneq  28670  ncolncol  28672  coltr3  28674  mirln  28702  mirln2  28703  mirconn  28704  krippenlem  28716  footexALT  28744  footexlem1  28745  footexlem2  28746  colperpexlem3  28758  mideulem2  28760  opphllem  28761  oppne3  28769  opphllem1  28773  opphllem2  28774  opphllem4  28776  oppperpex  28779  opphl  28780  hlpasch  28782  hpgerlem  28791  colhp  28796  midbtwn  28805  lmieu  28810  lmiisolem  28822  sacgr  28857  f1otrg  28897  f1otrge  28898  ebtwntg  29015  ecgrtg  29016  eengtrkg  29019  eengtrkge  29020  upgr1eop  29150  usgredg3  29251  uspgr1eop  29282  usgr1eop  29285  vtxdun  29517  vtxdfiun  29518  1loopgruspgr  29536  1loopgrvd2  29539  1hevtxdg1  29542  1egrvtxdg1  29545  1egrvtxdg0  29547  umgr2v2e  29561  wlkres  29706  wlkp1lem4  29712  wlkp1  29717  wwlksm1edg  29914  wwlksnext  29926  wwlksnextproplem3  29944  clwwlkel  30078  1wlkdlem2  30170  trlsegvdeg  30259  eupth2lem3lem1  30260  eupth2lem3lem2  30261  extwwlkfab  30384  numclwlk2lem2f  30409  spansnid  31595  elspansn4  31605  fnpreimac  32689  ccatf1  32915  ccatws1f1olast  32919  swrdrn2  32921  swrdrn3  32922  swrdf1  32923  splfv3  32925  pwrssmgc  32973  pfxchn  32982  chnind  32983  chnub  32984  chnlt  32985  wrdpmtrlast  33086  psgnfzto1stlem  33093  cycpmfv1  33106  cycpmfv2  33107  cycpmco2lem2  33120  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  cyc3co2  33133  cycpmrn  33136  submarchi  33166  subrdom  33254  fracfld  33275  imaslmod  33346  quslmod  33351  quslmhm  33352  nsgqusf1olem2  33407  lmhmqusker  33410  rhmquskerlem  33418  idlinsubrg  33424  drngidl  33426  rhmpreimaprmidl  33444  qsidomlem2  33446  mxidlprm  33463  opprmxidlabs  33480  qsdrngilem  33487  qsdrngi  33488  qsdrnglem2  33489  idlsrg0g  33499  pidufd  33536  dfufd2lem  33542  fply1  33549  evl1fpws  33555  ressply1sub  33560  ply1asclunit  33564  r1plmhm  33595  drgextlsp  33608  matdim  33628  ply1degltdimlem  33635  lindsunlem  33637  qusdimsum  33641  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33676  evls1fldgencl  33680  irngss  33687  irngnzply1  33691  minplymindeg  33701  minplyirredlem  33703  irredminply  33707  algextdeglem2  33709  constrconj  33735  1smat1  33750  submat1n  33751  lmatfval  33760  lmatcl  33762  mdetpmtr1  33769  madjusmdetlem4  33776  qtopt1  33781  qtophaus  33782  locfinref  33787  zarcls1  33815  zarclsiin  33817  zarmxt1  33826  zarcmplem  33827  rhmpreimacn  33831  ordtrest2NEWlem  33868  elzrhunit  33925  qqhcn  33937  qqhucn  33938  esumel  34011  esumsplit  34017  sigagenss2  34114  elsx  34158  sxbrsigalem0  34236  dya2icoseg  34242  eulerpartlemb  34333  eulerpartlemgvv  34341  iwrdsplit  34352  sseqfv2  34359  probfinmeasb  34393  dstrvprob  34436  dstfrvel  34438  ballotlemrv  34484  signstfvn  34546  signstfvp  34548  signstfveq0  34554  signsvtp  34560  signsvtn  34561  reprsuc  34592  reprpmtf1o  34603  lpadleft  34660  bnj1006  34936  bnj1018g  34939  bnj1018  34940  bnj1121  34961  bnj1398  35010  bnj1450  35026  bnj1501  35043  revpfxsfxrev  35083  swrdrevpfx  35084  pfxwlk  35091  revwlk  35092  swrdwlk  35094  subfacp1lem5  35152  ptpconn  35201  indispconn  35202  cvxsconn  35211  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem12  35282  satfv1lem  35330  satffunlem1lem2  35371  satffunlem2lem2  35374  satefvfmla1  35393  mrsubcv  35478  mrsubff  35480  mrsubrn  35481  mrsubccat  35486  elmrsubrn  35488  mrsubco  35489  mrsubvrs  35490  mvhf  35526  msubvrs  35528  mclsax  35537  r1peuqusdeg1  35611  linerflx1  36113  linerflx2  36115  fwddifnval  36127  elhf2  36139  neibastop2lem  36326  weiunpo  36431  weiunso  36432  icoreunrn  37325  relowlssretop  37329  sucneqond  37331  matunitlindflem2  37577  poimirlem4  37584  poimirlem20  37600  poimirlem30  37610  broucube  37614  opnmbllem0  37616  areacirclem2  37669  areacirclem4  37671  blssp  37716  sstotbnd2  37734  totbndbnd  37749  prdstotbnd  37754  cnpwstotbnd  37757  heiborlem9  37779  exidcl  37836  exidresid  37839  grpokerinj  37853  iscringd  37958  erimeq2  38634  prter3  38838  toycom  38929  islfld  39018  lshpsmreu  39065  ldualelvbase  39083  ldualssvscl  39114  lkreqN  39126  lkrlspeqN  39127  erng1lem  40944  erngdvlem4  40948  erng0g  40951  erng1r  40952  erngdvlem4-rN  40956  dva0g  40984  dia1dim2  41019  dia1dimid  41020  dia2dimlem5  41025  dvhelvbasei  41045  dvhvaddass  41054  tendoinvcl  41061  tendolinv  41062  tendorinv  41063  dvhgrp  41064  dvhlveclem  41065  cdlemn4  41155  lcfrlem12N  41511  lcfrlem15  41514  lcdvscl  41562  lcdlssvscl  41563  lcdvsass  41564  lcdvs0N  41573  mapdincl  41618  mapdin  41619  mapdlsmcl  41620  mapdcnvatN  41623  mapdpglem2  41630  mapdpglem12  41640  mapdpglem18  41646  mapdpglem21  41649  mapdpglem22  41650  mapdpglem28  41658  mapdpglem30  41659  hdmaprnlem3N  41807  hdmaprnlem3uN  41808  hdmaprnlem7N  41812  hdmaprnlem8N  41813  hdmaprnlem9N  41814  hdmaprnlem3eN  41815  hdmaprnlem16N  41819  hgmapdcl  41847  hgmapval1  41850  hgmaprnlem4N  41856  hdmapinvlem1  41875  fzadd2d  41934  aks6d1c2lem4  42084  sticksstones1  42103  sticksstones8  42110  sticksstones9  42111  sticksstones10  42112  sticksstones11  42113  sticksstones17  42120  sticksstones18  42121  aks6d1c6lem4  42130  rhmqusspan  42142  aks5lem2  42144  fnsnbt  42225  mhmcopsr  42504  evlsbagval  42521  evlsevl  42526  evlvvval  42528  evlvvvallem  42529  selvcllem2  42533  evlselv  42542  mhpind  42549  fltnltalem  42617  wepwsolem  42999  kercvrlsm  43040  dfacbasgrp  43065  onexomgt  43202  onexoegt  43205  onov0suclim  43236  cantnftermord  43282  cantnf2  43287  omcl2  43295  ofoaf  43317  ofoafo  43318  imo72b2lem0  44127  grurankcld  44202  grumnudlem  44254  grumnud  44255  inaex  44266  gruex  44267  dvconstbi  44303  cncmpmax  44932  iooabslt  45417  fmul01lt1lem2  45506  limciccioolb  45542  limcicciooub  45558  limsuppnfdlem  45622  climrescn  45669  climxrrelem  45670  climxrre  45671  liminflimsupxrre  45738  xlimmnfvlem2  45754  xlimpnfvlem2  45758  fsumcncf  45799  ioccncflimc  45806  icocncflimc  45810  cncfiooicclem1  45814  dvbdfbdioolem2  45850  dvnmul  45864  stoweidlem26  45947  stoweidlem34  45955  stoweidlem48  45969  stoweidlem59  45980  dirkercncflem3  46026  fourierdlem32  46060  fourierdlem41  46069  fourierdlem51  46078  fourierdlem63  46090  fourierdlem82  46109  fourierdlem85  46112  fourierdlem93  46120  fourierdlem111  46138  fourierdlem114  46141  etransclem35  46190  hspdifhsp  46537  opnvonmbllem1  46553  ovnovollem1  46577  mbfresmf  46660  smfaddlem1  46684  smfsuplem1  46732  smflimsuplem5  46745  setsidel  47250  setsnidel  47251  imasetpreimafvbijlemf  47275  prelspr  47360  rngccatidALTV  47995  rhmsubcALTVlem3  48006  funcringcsetcALTV2lem3  48015  funcringcsetcALTV2lem8  48020  ringccatidALTV  48029  funcringcsetclem3ALTV  48038  funcringcsetclem8ALTV  48043  srhmsubcALTVlem1  48046  srhmsubcALTV  48048  lcosslsp  48167  nnolog2flm1  48324  glbprlem  48645  topdlat  48676  catprs  48678  mndtccatid  48760  grptcmon  48763  grptcepi  48764