Theorem eleqtrrd 2866

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is used by:  3eltr4d  2878  rspc2vd  3901  disjxiun  5106  eldmressnsn  6023  fnsnbg  7162  elimdelov  7506  elovmpt3rab1  7670  fnwelem  8123  tfrlem13  8373  tz7.44-2  8390  omordi  8547  oneo  8562  omeulem2  8564  oeordi  8569  oeeui  8584  nnneo  8637  naddelim  8669  erref  8711  en1uniel  9022  omxpenlem  9062  unblem3  9250  dffi3  9387  ordtypelem10  9485  oismo  9498  cantnff  9639  cantnfp1lem3  9645  cantnflem1  9654  cnfcom  9665  r1ordg  9746  r1pwss  9752  rankwflemb  9761  r1elwf  9764  rankidb  9768  rankonidlem  9796  fseqenlem2  10014  dfac12lem1  10132  dfac12lem2  10133  pwsdompw  10191  ackbij2lem3  10228  ackbij2  10230  cfsmolem  10258  hsmexlem4  10417  ttukeylem3  10499  ttukeylem7  10503  iundom2g  10528  fpwwe2lem8  10627  canthwelem  10639  pwfseqlem4  10651  winalim2  10685  r1wunlim  10726  tskmid  10829  fzopth  13594  predfz  13686  fzoss2  13721  fz1fzo0m1  13744  fzo0addel  13752  fzo0addelr  13753  elfzoext  13756  fzosubel3  13760  elfzomin  13771  elfzonlteqm1  13775  fzoend  13791  fzoopth  13796  fzofzp1  13798  fzofzp1b  13799  peano2fzor  13809  zmodfzo  13932  seqf1olem2  14083  bcn2  14360  swrdccat2  14712  pfxccat1  14744  swrdswrd  14747  pfxccatin12  14775  splfv1  14797  revcl  14803  revlen  14804  revccat  14808  revrev  14809  repswpfx  14827  cshwidxmod  14845  revco  14876  limsupgre  15537  summolem2a  15771  fsumm1  15807  fsumcom2  15830  prodmolem2a  15993  fprodm1  16026  fprodcom2  16043  prmreclem4  16983  prmreclem5  16984  vdwapid1  17039  vdwlem5  17049  vdwlem8  17052  vdwnnlem2  17060  ramub1lem1  17090  ramub1lem2  17091  mrieqvlemd  17689  mreexd  17702  mreexexlemd  17704  catcocl  17745  catass  17746  moni  17797  epii  17804  inviso1  17827  episect  17846  invisoinvl  17851  catsubcat  17900  subccocl  17906  fullsubc  17911  funcco  17932  resf2nd  17956  funcres  17957  fthepi  17991  nati  18019  arwhoma  18106  catccatid  18167  resscatc  18170  catcisolem  18171  catcoppccl  18178  catcfuccl  18179  estrreslem2  18198  funcestrcsetclem3  18202  funcestrcsetclem8  18207  equivestrcsetc  18212  funcsetcestrclem3  18216  funcsetcestrclem8  18222  xpcco  18243  xpcco2  18247  xpccatid  18248  prfcl  18263  catcxpccl  18267  curf12  18287  curf1cl  18288  curf2  18289  curf2cl  18291  curfcl  18292  uncf2  18297  uncfcurf  18299  diag12  18304  diag2  18305  curf2ndf  18307  hofcl  18319  oppchofcl  18320  oyoncl  18330  yonedalem3a  18334  yonedalem4b  18336  yonedalem22  18338  yonedalem3b  18339  yonedalem3  18340  yonedainv  18341  yonffthlem  18342  latcl2  18496  latlem  18497  latjcom  18507  latmcom  18523  clatlem  18562  clatlubcl2  18564  clatglbcl2  18566  acsfiindd  18613  pfxchn  18670  chnind  18681  chnub  18682  chnlt  18683  chnccat  18686  chnrev  18687  gsumpropd2lem  18741  sgrppropd  18793  mndpropd  18821  imasmnd  18837  frmdmnd  18922  frmdgsum  18925  grpsubpropd2  19116  imasgrp  19126  subg0  19202  0ghm  19304  resghm2  19307  ghmco  19310  pwsdiagghm  19318  ghmqusnsglem2  19355  ghmqusnsg  19356  ghmquskerlem2  19359  ghmquskerlem3  19360  ghmqusker  19361  psgnunilem1  19567  psgnunilem5  19568  psgnunilem2  19569  psgnunilem3  19570  sylow1lem4  19675  sylow1lem5  19676  efglem  19790  efgtf  19796  efginvrel2  19801  efginvrel1  19802  efgsdmi  19806  efgs1b  19810  efgsres  19812  efgsfo  19813  efgredleme  19817  efgredlemc  19819  efgredlem  19821  efgcpbllemb  19829  frgp0  19834  frgpadd  19837  frgpinv  19838  vrgpf  19842  vrgpinv  19843  frgpuplem  19846  frgpup1  19849  frgpup2  19850  frgpup3lem  19851  frgpnabllem1  19947  frgpnabllem2  19948  gsumval3  19981  dprdfid  20093  dprdsn  20112  dprd2da  20118  dpjidcl  20134  pgpfac1lem2  20151  pgpfaclem3  20159  ablsimpg1gend  20181  ablsimpgprmd  20191  rngpropd  20256  imasrng  20259  ringpropd  20376  imasring  20417  qusring2  20421  pwsco1rhm  20598  pwsco2rhm  20599  lringuplu  20652  subrgunit  20698  pwsdiagrhm  20715  rnghmsubcsetclem1  20739  zrinitorngc  20750  zrtermorngc  20751  zrzeroorngc  20752  rhmsubcsetclem1  20768  rhmsubcrngclem1  20774  zrtermoringc  20783  zrninitoringc  20784  srhmsubclem2  20786  srhmsubc  20788  cntzsdrg  20914  isabvd  20924  lmodprop2d  21054  islssd  21065  prdsvscacl  21098  prdslmodd  21099  islmhm2  21168  lmhmco  21173  lmhmplusg  21174  lmhmvsca  21175  lmhmpropd  21203  lsppreli  21220  ellspsn4  21257  lssacsex  21277  lspsnat  21278  lidlnsg  21391  drngidl  21394  qus2idrng  21421  qus1  21422  qusrhm  21424  rhmpreimaidl  21425  rhmqusnsg  21434  rngqiprngghmlem1  21436  rngqiprngfulem1  21460  rhmpreimaprmidl  21488  qsidomlem2  21490  irinitoringc  21638  nzerooringczr  21639  znf1o  21710  cssmre  21852  dsmmlss  21903  frlmsplit2  21932  frlmbas3  21935  frlmup1  21957  assapropd  22030  psr0cl  22111  psrnegcl  22113  psr1cl  22119  resspsrmul  22134  subrgpsr  22136  mvrf  22143  mplmon  22195  mplcoe1  22197  subrgasclcl  22227  mplind  22230  evlslem1  22242  mhmcompl  22281  evlsevl  22292  evlvvval  22293  selvcllem2  22295  subrgply1  22401  psrplusgpropd  22404  ply1coe  22467  cply1coe0bi  22471  lply1binomsc  22480  ply1fermltlchr  22481  evls1val  22489  evls1rhm  22491  evl1val  22498  evl1rhm  22501  pf1ind  22524  evl1scvarpw  22532  evls1fpws  22538  rhmply1  22552  matbas2i  22588  matplusg2  22593  matvsca2  22594  matsubgcell  22600  matvscacell  22602  mpomatmul  22612  mavmulval  22711  mavmulcl  22713  mavmulass  22715  mavmul0  22718  mavmumamul1  22721  m1detdiag  22763  cramerimplem2  22850  mat2pmatmul  22897  mat2pmatlin  22901  monmatcollpw  22945  pmatcollpwfi  22948  mply1topmatcl  22971  pm2mpghm  22982  pm2mpmhmlem2  22985  pm2mp  22991  chpmat1dlem  23001  chpmat1d  23002  chpdmatlem0  23003  chpscmat  23008  chpscmatgsumbin  23010  chpscmatgsummon  23011  chfacfscmulcl  23023  cpmadugsumlemB  23040  cpmadugsumlemC  23041  chcoeffeqlem  23051  cldmreon  23260  neiptopreu  23299  maxlp  23313  ordttopon  23359  ordtrest2lem  23369  cnprcl2  23417  lmcnp  23470  resthauslem  23529  hauscmplem  23572  1stcfb  23611  2ndcctbss  23621  2ndcomap  23624  dis2ndc  23626  loclly  23653  hausllycmp  23660  locfincmp  23692  dissnref  23694  kgeni  23703  kgenidm  23713  ptpjpre2  23746  xkoopn  23755  txopn  23768  ptpjopn  23778  ptcldmpt  23780  ptcls  23782  pthaus  23804  txkgen  23818  xkohaus  23819  xkopt  23821  txconn  23855  imastps  23887  kqid  23894  kqopn  23900  kqcld  23901  isr0  23903  indishmph  23964  pt1hmeo  23972  ptuncnv  23973  ptunhmeo  23974  t0kq  23984  filconn  24049  uzrest  24063  uffixsn  24091  fmfnfmlem2  24121  flimss2  24138  flimss1  24139  flimclslem  24150  flfcnp  24170  fclsfnflim  24193  uffclsflim  24197  fcfelbas  24202  alexsublem  24210  alexsub  24211  cnextcn  24233  cnextfres1  24234  cnextfres  24235  tmdgsum  24261  distgp  24265  indistgp  24266  symgtgp  24272  ghmcnp  24281  qustgpopn  24286  qustgplem  24287  qustgphaus  24289  prdstmdd  24290  prdstgpd  24291  tsmsid  24306  tsmssubm  24309  tsmsmhm  24312  tsmsadd  24313  tsmssplit  24318  utop2nei  24416  utop3cls  24417  neipcfilu  24461  cnextucn  24468  ucnextcn  24469  blpnfctr  24602  lpbl  24669  met2ndci  24688  tmsxps  24702  metcnpi  24710  metcnpi2  24711  metcnpi3  24712  metustid  24720  metustsym  24721  metustexhalf  24722  subgngp  24801  ngptgp  24802  sranlm  24850  nlmvscn  24853  nrginvrcn  24858  lssnlm  24867  nghmcn  24911  iccntr  24988  icccmplem2  24990  msdcn  25008  cncfmptc  25080  cncfmptid  25081  cncfmpt2f  25083  icoopnst  25107  iocopnst  25108  nmoleub2lem3  25283  nmoleub3  25287  nmhmcn  25288  ipcn  25414  cfilfcls  25442  caucfil  25451  equivcau  25468  caubl  25476  flimcfil  25482  cmssmscld  25518  rrxdstprj1  25577  minveclem3b  25596  minveclem4  25600  mulcncf  25614  ovolicc2lem3  25687  ovolicc2lem4  25688  opnmbllem  25769  vitalilem2  25777  mbfsup  25832  mbfinf  25833  mbfi1fseqlem4  25886  limccnp  26059  limccnp2  26060  dvreslem  26077  dvres2lem  26078  dvidlem  26083  dvcnp2  26088  dvcn  26089  dvaddbr  26106  dvmulbr  26107  dvcmul  26112  dvcof  26116  dvcnvlem  26144  dvef  26148  rollelem  26157  dvlip2  26163  dvivthlem1  26176  dvivth  26178  lhop2  26183  lhop  26184  dvcnvrelem1  26185  dvcnvrelem2  26186  dvcnvre  26187  ply1rem  26332  fta1blem  26337  plycpn  26459  plyrem  26475  tayl0  26534  dvtaylp  26542  dvntaylp  26543  dvntaylp0  26544  taylthlem1  26545  taylthlem2  26546  ulmdvlem3  26574  psercn  26598  pserdv  26601  abelth  26613  efabl  26724  efopnlem1  26830  loglesqrt  26935  relogbf  26965  efrlim  27143  dchrghm  27429  dchrptlem3  27439  nodenselem5  27861  nosupres  27880  noinfres  27895  ltslpss  28110  precsexlem11  28419  noseq0  28492  noseqp1  28493  noseqrdgfn  28508  noseqrdgsuc  28510  tgbtwntriv2  28765  tgbtwnne  28768  ercgrg  28795  tgidinside  28849  tgbtwnconn1  28853  tglnne  28910  tglinesseq  28922  tglnne0  28923  tglineneq  28927  ncolncol  28929  coltr3  28931  tglnpt2  28935  tglnpt3  28936  mirln  28962  mirln2  28963  mirconn  28964  krippenlem  28976  footexALT  29007  footexlem1  29008  footexlem2  29009  colperpexlem3  29022  mideulem2  29024  opphllem  29025  oppne3  29033  opphllem1  29037  opphllem2  29038  opphllem4  29040  oppperpex  29043  opphl  29044  hlpasch  29047  hpgerlem  29056  colhp  29061  plngval  29068  lnincplng  29075  plngrotlem1  29078  lnssplnglem  29082  plng3p  29088  midbtwn  29097  lmieu  29102  lmiisolem  29114  sacgr  29151  perpeqlem  29159  prlnghpg  29205  prlngmolem1  29211  prlngmid2  29220  prlngsymquadopp  29224  quadcgrprlng  29225  f1otrg  29229  f1otrge  29230  ebtwntg  29341  ecgrtg  29342  eengtrkg  29345  eengtrkge  29346  upgr1eop  29474  usgredg3  29575  uspgr1eop  29606  usgr1eop  29609  vtxdun  29840  vtxdfiun  29841  1loopgruspgr  29859  1loopgrvd2  29862  1hevtxdg1  29865  1egrvtxdg1  29868  1egrvtxdg0  29870  umgr2v2e  29884  wlkres  30027  wlkp1lem4  30033  wlkp1  30038  cyclnumvtx  30158  wwlksm1edg  30239  wwlksnext  30251  wwlksnextproplem3  30269  clwwlkel  30406  1wlkdlem2  30498  trlsegvdeg  30587  eupth2lem3lem1  30588  eupth2lem3lem2  30589  extwwlkfab  30712  numclwlk2lem2f  30737  spansnid  31924  elspansn4  31934  fnpreimac  33024  ccatf1  33278  ccatws1f1olast  33281  swrdrn2  33283  swrdrn3  33284  swrdf1  33285  splfv3  33287  pwrssmgc  33329  suppgsumssiun  33401  wrdpmtrlast  33422  psgnfzto1stlem  33429  cycpmfv1  33442  cycpmfv2  33443  cycpmco2lem2  33456  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2  33462  cyc3co2  33469  cycpmrn  33472  submarchi  33515  subrdom  33614  fracfld  33638  imaslmod  33682  quslmod  33687  quslmhm  33688  nsgqusf1olem2  33732  lmhmqusker  33735  rhmquskerlem  33742  idlinsubrg  33748  mxidlprm  33762  opprmxidlabs  33778  qsdrngilem  33785  qsdrngi  33786  qsdrnglem2  33787  idlsrg0g  33805  pidufd  33842  dfufd2lem  33848  fply1  33857  evl1fpws  33863  ressply1evls1  33864  ressply1sub  33869  ply1asclunit  33873  r1plmhm  33908  0mplrim  33913  selvascl  33916  selvply1rhmlema  33917  selvply1rhmlem1  33919  extvfvcl  33935  evlextv  33941  mplvrpmga  33944  psrmon  33948  psrmonprod  33951  mplmonprod  33953  issply  33960  esplympl  33966  esplyind  33974  drgextlsp  33993  matdim  34014  ply1degltdimlem  34021  lindsunlem  34023  qusdimsum  34027  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  extdg1id  34065  evls1fldgencl  34069  irngss  34086  irngnzply1  34090  extdgfialglem1  34091  extdgfialglem2  34092  minplymindeg  34107  minplyirredlem  34109  irredminply  34115  algextdeglem2  34117  constrconj  34144  constrfiss  34150  1smat1  34203  submat1n  34204  lmatfval  34213  lmatcl  34215  mdetpmtr1  34222  madjusmdetlem4  34229  qtopt1  34234  qtophaus  34235  locfinref  34240  zarcls1  34268  zarclsiin  34270  zarmxt1  34279  zarcmplem  34280  rhmpreimacn  34284  ordtrest2NEWlem  34321  elzrhunit  34376  qqhcn  34390  qqhucn  34391  esumel  34446  esumsplit  34452  sigagenss2  34549  elsx  34593  sxbrsigalem0  34670  dya2icoseg  34676  eulerpartlemb  34767  eulerpartlemgvv  34775  iwrdsplit  34786  sseqfv2  34793  probfinmeasb  34827  dstrvprob  34871  dstfrvel  34873  ballotlemrv  34919  signstfvn  34965  signstfvp  34967  signstfveq0  34973  signsvtp  34979  signsvtn  34980  reprsuc  35011  reprpmtf1o  35022  morleylemrneab  35067  lpadleft  35082  bnj1006  35357  bnj1018g  35360  bnj1018  35361  bnj1121  35382  bnj1398  35431  bnj1450  35447  bnj1501  35464  revpfxsfxrev  35615  swrdrevpfx  35616  pfxwlk  35624  revwlk  35625  swrdwlk  35627  subfacp1lem5  35684  ptpconn  35733  indispconn  35734  cvxsconn  35743  cvmseu  35776  cvmliftmolem2  35782  cvmliftlem7  35791  cvmliftlem10  35794  cvmliftlem13  35796  cvmlift2lem12  35814  satfv1lem  35862  satffunlem1lem2  35903  satffunlem2lem2  35906  satefvfmla1  35925  mrsubcv  36010  mrsubff  36012  mrsubrn  36013  mrsubccat  36018  elmrsubrn  36020  mrsubco  36021  mrsubvrs  36022  mvhf  36058  msubvrs  36060  mclsax  36069  r1peuqusdeg1  36143  linerflx1  36649  linerflx2  36651  fwddifnval  36663  elhf2  36675  nadddilem3  36722  neibastop2lem  36899  weiunpo  37004  weiunso  37005  icoreunrn  38033  relowlssretop  38037  sucneqond  38039  matunitlindflem2  38296  poimirlem4  38303  poimirlem20  38319  poimirlem30  38329  broucube  38333  opnmbllem0  38335  areacirclem2  38388  areacirclem4  38390  blssp  38435  sstotbnd2  38453  totbndbnd  38468  prdstotbnd  38473  cnpwstotbnd  38476  heiborlem9  38498  exidcl  38555  exidresid  38558  grpokerinj  38572  iscringd  38677  erimeq2  39440  prter3  39684  toycom  39775  islfld  39864  lshpsmreu  39911  ldualelvbase  39929  ldualssvscl  39960  lkreqN  39972  lkrlspeqN  39973  erng1lem  41789  erngdvlem4  41793  erng0g  41796  erng1r  41797  erngdvlem4-rN  41801  dva0g  41829  dia1dim2  41864  dia1dimid  41865  dia2dimlem5  41870  dvhelvbasei  41890  dvhvaddass  41899  tendoinvcl  41906  tendolinv  41907  tendorinv  41908  dvhgrp  41909  dvhlveclem  41910  cdlemn4  42000  lcfrlem12N  42356  lcfrlem15  42359  lcdvscl  42407  lcdlssvscl  42408  lcdvsass  42409  lcdvs0N  42418  mapdincl  42463  mapdin  42464  mapdlsmcl  42465  mapdcnvatN  42468  mapdpglem2  42475  mapdpglem12  42485  mapdpglem18  42491  mapdpglem21  42494  mapdpglem22  42495  mapdpglem28  42503  mapdpglem30  42504  hdmaprnlem3N  42652  hdmaprnlem3uN  42653  hdmaprnlem7N  42657  hdmaprnlem8N  42658  hdmaprnlem9N  42659  hdmaprnlem3eN  42660  hdmaprnlem16N  42664  hgmapdcl  42692  hgmapval1  42695  hgmaprnlem4N  42701  hdmapinvlem1  42720  fzadd2d  42774  aks6d1c2lem4  42922  sticksstones1  42941  sticksstones8  42948  sticksstones9  42949  sticksstones10  42950  sticksstones11  42951  sticksstones17  42958  sticksstones18  42959  aks6d1c6lem4  42968  rhmqusspan  42980  aks5lem2  42982  mhmcopsr  43340  evlsbagval  43346  evlvvvallem  43347  evlselv  43349  mhpind  43354  fltnltalem  43422  wepwsolem  43797  kercvrlsm  43838  dfacbasgrp  43863  onexomgt  43996  onexoegt  43999  onov0suclim  44029  cantnftermord  44075  cantnf2  44080  omcl2  44088  ofoaf  44110  ofoafo  44111  grurankcld  44985  grumnudlem  45023  grumnud  45024  inaex  45035  gruex  45036  dvconstbi  45072  cncmpmax  45780  iooabslt  46243  fmul01lt1lem2  46329  limciccioolb  46365  limcicciooub  46379  limsuppnfdlem  46443  climrescn  46490  climxrrelem  46491  climxrre  46492  liminflimsupxrre  46559  xlimmnfvlem2  46575  xlimpnfvlem2  46579  fsumcncf  46620  ioccncflimc  46627  cncfuni  46628  icocncflimc  46631  cncfiooicclem1  46635  dvbdfbdioolem2  46671  dvnmul  46685  dvnprodlem1  46688  stoweidlem26  46768  stoweidlem34  46776  stoweidlem48  46790  stoweidlem59  46801  dirkercncflem3  46847  fourierdlem32  46881  fourierdlem41  46890  fourierdlem51  46899  fourierdlem63  46911  fourierdlem82  46930  fourierdlem85  46933  fourierdlem93  46941  fourierdlem111  46959  fourierdlem114  46962  etransclem35  47011  hoicvr  47290  hspdifhsp  47358  opnvonmbllem1  47374  ovnovollem1  47398  mbfresmf  47481  smfaddlem1  47505  smfsuplem1  47553  smflimsuplem5  47566  chnerlem2  47627  setsidel  48153  setsnidel  48154  imasetpreimafvbijlemf  48178  prelspr  48263  upgrimpths  48702  gpgprismgr4cycllem9  48896  rngccatidALTV  49065  rhmsubcALTVlem3  49076  funcringcsetcALTV2lem3  49085  funcringcsetcALTV2lem8  49090  ringccatidALTV  49099  funcringcsetclem3ALTV  49108  funcringcsetclem8ALTV  49113  srhmsubcALTVlem1  49116  srhmsubcALTV  49118  lcosslsp  49246  nnolog2flm1  49398  ffvbr  49662  glbprlem  49771  topdlat  49810  catprs  49817  iinfsubc  49864  iinfconstbaslem  49871  imaid  49960  fthcomf  49963  uptr2  50027  natoppf2  50036  natoppfb  50037  swapf2  50080  swapfiso  50091  swapciso  50092  oppc1stflem  50093  cofuswapf2  50101  fuco22natlem  50151  fucoppcffth  50217  oppcthinco  50245  oppcthinendcALT  50247  thinccisod  50260  termco  50287  termchommo  50291  termcid  50292  termcterm  50319  termcterm2  50320  diagciso  50345  diagcic  50346  funcsn  50347  uobeqterm  50352  mndtccatid  50393  grptcmon  50399  grptcepi  50400  2arwcat  50406  lanval2  50433  ranval2  50436  lanup  50447  ranup  50448  lmddu  50473