Theorem eleqtrrd 2837

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  3eltr4d  2849  rspc2vd  3895  disjxiun  5093  eldmressnsn  5981  fnsnbg  7108  elimdelov  7452  elovmpt3rab1  7616  fnwelem  8071  tfrlem13  8319  tz7.44-2  8336  omordi  8491  oneo  8506  omeulem2  8508  oeordi  8513  oeeui  8528  nnneo  8581  naddelim  8612  erref  8653  en1uniel  8964  omxpenlem  9004  unblem3  9192  dffi3  9332  ordtypelem10  9430  oismo  9443  cantnff  9581  cantnfp1lem3  9587  cantnflem1  9596  cnfcom  9607  r1ordg  9688  r1pwss  9694  rankwflemb  9703  r1elwf  9706  rankidb  9710  rankonidlem  9738  fseqenlem2  9933  dfac12lem1  10052  dfac12lem2  10053  pwsdompw  10111  ackbij2lem3  10148  ackbij2  10150  cfsmolem  10178  hsmexlem4  10337  ttukeylem3  10419  ttukeylem7  10423  iundom2g  10448  fpwwe2lem8  10547  canthwelem  10559  pwfseqlem4  10571  winalim2  10605  r1wunlim  10646  tskmid  10749  fzopth  13475  predfz  13567  fzoss2  13601  fz1fzo0m1  13624  fzo0addel  13632  fzo0addelr  13633  elfzoext  13636  fzosubel3  13640  elfzomin  13651  elfzonlteqm1  13655  fzoend  13671  fzoopth  13676  fzofzp1  13678  fzofzp1b  13679  peano2fzor  13689  zmodfzo  13812  seqf1olem2  13963  bcn2  14240  swrdccat2  14591  pfxccat1  14623  swrdswrd  14626  pfxccatin12  14654  splfv1  14676  revcl  14682  revlen  14683  revccat  14687  revrev  14688  repswpfx  14706  cshwidxmod  14724  revco  14755  limsupgre  15402  summolem2a  15636  fsumm1  15672  fsumcom2  15695  prodmolem2a  15855  fprodm1  15888  fprodcom2  15905  prmreclem4  16845  prmreclem5  16846  vdwapid1  16901  vdwlem5  16911  vdwlem8  16914  vdwnnlem2  16922  ramub1lem1  16952  ramub1lem2  16953  mrieqvlemd  17550  mreexd  17563  mreexexlemd  17565  catcocl  17606  catass  17607  moni  17658  epii  17665  inviso1  17688  episect  17707  invisoinvl  17712  catsubcat  17761  subccocl  17767  fullsubc  17772  funcco  17793  resf2nd  17817  funcres  17818  fthepi  17852  nati  17880  arwhoma  17967  catccatid  18028  resscatc  18031  catcisolem  18032  catcoppccl  18039  catcfuccl  18040  estrreslem2  18059  funcestrcsetclem3  18063  funcestrcsetclem8  18068  equivestrcsetc  18073  funcsetcestrclem3  18077  funcsetcestrclem8  18083  xpcco  18104  xpcco2  18108  xpccatid  18109  prfcl  18124  catcxpccl  18128  curf12  18148  curf1cl  18149  curf2  18150  curf2cl  18152  curfcl  18153  uncf2  18158  uncfcurf  18160  diag12  18165  diag2  18166  curf2ndf  18168  hofcl  18180  oppchofcl  18181  oyoncl  18191  yonedalem3a  18195  yonedalem4b  18197  yonedalem22  18199  yonedalem3b  18200  yonedalem3  18201  yonedainv  18202  yonffthlem  18203  latcl2  18357  latlem  18358  latjcom  18368  latmcom  18384  clatlem  18423  clatlubcl2  18425  clatglbcl2  18427  acsfiindd  18474  pfxchn  18531  chnind  18542  chnub  18543  chnlt  18544  chnccat  18547  chnrev  18548  gsumpropd2lem  18602  sgrppropd  18654  mndpropd  18682  imasmnd  18698  frmdmnd  18782  frmdgsum  18785  grpsubpropd2  18974  imasgrp  18984  subg0  19060  0ghm  19157  resghm2  19160  ghmco  19163  pwsdiagghm  19171  ghmqusnsglem2  19208  ghmqusnsg  19209  ghmquskerlem2  19212  ghmquskerlem3  19213  ghmqusker  19214  psgnunilem1  19420  psgnunilem5  19421  psgnunilem2  19422  psgnunilem3  19423  sylow1lem4  19528  sylow1lem5  19529  efglem  19643  efgtf  19649  efginvrel2  19654  efginvrel1  19655  efgsdmi  19659  efgs1b  19663  efgsres  19665  efgsfo  19666  efgredleme  19670  efgredlemc  19672  efgredlem  19674  efgcpbllemb  19682  frgp0  19687  frgpadd  19690  frgpinv  19691  vrgpf  19695  vrgpinv  19696  frgpuplem  19699  frgpup1  19702  frgpup2  19703  frgpup3lem  19704  frgpnabllem1  19800  frgpnabllem2  19801  gsumval3  19834  dprdfid  19946  dprdsn  19965  dprd2da  19971  dpjidcl  19987  pgpfac1lem2  20004  pgpfaclem3  20012  ablsimpg1gend  20034  ablsimpgprmd  20044  rngpropd  20107  imasrng  20110  ringpropd  20221  imasring  20264  qusring2  20268  pwsco1rhm  20433  pwsco2rhm  20434  lringuplu  20475  subrgunit  20521  pwsdiagrhm  20538  rnghmsubcsetclem1  20562  zrinitorngc  20573  zrtermorngc  20574  zrzeroorngc  20575  rhmsubcsetclem1  20591  rhmsubcrngclem1  20597  zrtermoringc  20606  zrninitoringc  20607  srhmsubclem2  20609  srhmsubc  20611  cntzsdrg  20733  isabvd  20743  lmodprop2d  20873  islssd  20884  prdsvscacl  20917  prdslmodd  20918  islmhm2  20988  lmhmco  20993  lmhmplusg  20994  lmhmvsca  20995  lmhmpropd  21023  lsppreli  21040  ellspsn4  21077  lssacsex  21097  lspsnat  21098  lidlnsg  21201  qus2idrng  21226  qus1  21227  qusrhm  21229  rhmpreimaidl  21230  rhmqusnsg  21238  rngqiprngghmlem1  21240  rngqiprngfulem1  21264  irinitoringc  21432  nzerooringczr  21433  znf1o  21504  cssmre  21646  dsmmlss  21697  frlmsplit2  21726  frlmbas3  21729  frlmup1  21751  assapropd  21825  psr0cl  21906  psrnegcl  21908  psr1cl  21914  resspsrmul  21929  subrgpsr  21931  mvrf  21938  mplmon  21988  mplcoe1  21990  subrgasclcl  22020  mplind  22023  evlslem1  22035  subrgply1  22171  psrplusgpropd  22174  ply1coe  22240  cply1coe0bi  22244  lply1binomsc  22253  ply1fermltlchr  22254  evls1val  22262  evls1rhm  22264  evl1val  22271  evl1rhm  22274  pf1ind  22297  evl1scvarpw  22305  evls1fpws  22311  mhmcompl  22322  rhmply1  22328  matbas2i  22364  matplusg2  22369  matvsca2  22370  matsubgcell  22376  matvscacell  22378  mpomatmul  22388  mavmulval  22487  mavmulcl  22489  mavmulass  22491  mavmul0  22494  mavmumamul1  22497  m1detdiag  22539  cramerimplem2  22626  mat2pmatmul  22673  mat2pmatlin  22677  monmatcollpw  22721  pmatcollpwfi  22724  mply1topmatcl  22747  pm2mpghm  22758  pm2mpmhmlem2  22761  pm2mp  22767  chpmat1dlem  22777  chpmat1d  22778  chpdmatlem0  22779  chpscmat  22784  chpscmatgsumbin  22786  chpscmatgsummon  22787  chfacfscmulcl  22799  cpmadugsumlemB  22816  cpmadugsumlemC  22817  chcoeffeqlem  22827  cldmreon  23036  neiptopreu  23075  maxlp  23089  ordttopon  23135  ordtrest2lem  23145  cnprcl2  23193  lmcnp  23246  resthauslem  23305  hauscmplem  23348  1stcfb  23387  2ndcctbss  23397  2ndcomap  23400  dis2ndc  23402  loclly  23429  hausllycmp  23436  locfincmp  23468  dissnref  23470  kgeni  23479  kgenidm  23489  ptpjpre2  23522  xkoopn  23531  txopn  23544  ptpjopn  23554  ptcldmpt  23556  ptcls  23558  pthaus  23580  txkgen  23594  xkohaus  23595  xkopt  23597  txconn  23631  imastps  23663  kqid  23670  kqopn  23676  kqcld  23677  isr0  23679  indishmph  23740  pt1hmeo  23748  ptuncnv  23749  ptunhmeo  23750  t0kq  23760  filconn  23825  uzrest  23839  uffixsn  23867  fmfnfmlem2  23897  flimss2  23914  flimss1  23915  flimclslem  23926  flfcnp  23946  fclsfnflim  23969  uffclsflim  23973  fcfelbas  23978  alexsublem  23986  alexsub  23987  cnextcn  24009  cnextfres1  24010  cnextfres  24011  tmdgsum  24037  distgp  24041  indistgp  24042  symgtgp  24048  ghmcnp  24057  qustgpopn  24062  qustgplem  24063  qustgphaus  24065  prdstmdd  24066  prdstgpd  24067  tsmsid  24082  tsmssubm  24085  tsmsmhm  24088  tsmsadd  24089  tsmssplit  24094  utop2nei  24192  utop3cls  24193  neipcfilu  24237  cnextucn  24244  ucnextcn  24245  blpnfctr  24378  lpbl  24445  met2ndci  24464  tmsxps  24478  metcnpi  24486  metcnpi2  24487  metcnpi3  24488  metustid  24496  metustsym  24497  metustexhalf  24498  subgngp  24577  ngptgp  24578  sranlm  24626  nlmvscn  24629  nrginvrcn  24634  lssnlm  24643  nghmcn  24687  iccntr  24764  icccmplem2  24766  msdcn  24784  cncfmptc  24859  cncfmptid  24860  cncfmpt2f  24862  icoopnst  24890  iocopnst  24891  nmoleub2lem3  25069  nmoleub3  25073  nmhmcn  25074  ipcn  25200  cfilfcls  25228  caucfil  25237  equivcau  25254  caubl  25262  flimcfil  25268  cmssmscld  25304  rrxdstprj1  25363  minveclem3b  25382  minveclem4  25386  mulcncf  25400  ovolicc2lem3  25474  ovolicc2lem4  25475  opnmbllem  25556  vitalilem2  25564  mbfsup  25619  mbfinf  25620  mbfi1fseqlem4  25673  limccnp  25846  limccnp2  25847  dvreslem  25864  dvres2lem  25865  dvidlem  25870  dvcnp2  25875  dvcnp2OLD  25876  dvcn  25877  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvcmul  25901  dvcof  25906  dvcnvlem  25934  dvef  25938  rollelem  25947  dvlip2  25954  dvivthlem1  25967  dvivth  25969  lhop2  25974  lhop  25975  dvcnvrelem1  25976  dvcnvrelem2  25977  dvcnvre  25978  ply1rem  26125  fta1blem  26130  plycpn  26251  plyrem  26267  tayl0  26323  dvtaylp  26332  dvntaylp  26333  dvntaylp0  26334  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem3  26365  psercn  26390  pserdv  26393  abelth  26405  efabl  26513  efopnlem1  26619  loglesqrt  26725  relogbf  26755  efrlim  26933  efrlimOLD  26934  dchrghm  27221  dchrptlem3  27231  nodenselem5  27654  nosupres  27673  noinfres  27688  sltlpss  27880  precsexlem11  28185  noseq0  28251  noseqp1  28252  noseqrdgfn  28267  noseqrdgsuc  28269  tgbtwntriv2  28508  tgbtwnne  28511  ercgrg  28538  tgidinside  28592  tgbtwnconn1  28596  tglnne  28649  tglnne0  28661  tglnpt2  28662  tglineneq  28665  ncolncol  28667  coltr3  28669  mirln  28697  mirln2  28698  mirconn  28699  krippenlem  28711  footexALT  28739  footexlem1  28740  footexlem2  28741  colperpexlem3  28753  mideulem2  28755  opphllem  28756  oppne3  28764  opphllem1  28768  opphllem2  28769  opphllem4  28771  oppperpex  28774  opphl  28775  hlpasch  28777  hpgerlem  28786  colhp  28791  midbtwn  28800  lmieu  28805  lmiisolem  28817  sacgr  28852  f1otrg  28892  f1otrge  28893  ebtwntg  29004  ecgrtg  29005  eengtrkg  29008  eengtrkge  29009  upgr1eop  29137  usgredg3  29238  uspgr1eop  29269  usgr1eop  29272  vtxdun  29504  vtxdfiun  29505  1loopgruspgr  29523  1loopgrvd2  29526  1hevtxdg1  29529  1egrvtxdg1  29532  1egrvtxdg0  29534  umgr2v2e  29548  wlkres  29691  wlkp1lem4  29697  wlkp1  29702  cyclnumvtx  29822  wwlksm1edg  29903  wwlksnext  29915  wwlksnextproplem3  29933  clwwlkel  30070  1wlkdlem2  30162  trlsegvdeg  30251  eupth2lem3lem1  30252  eupth2lem3lem2  30253  extwwlkfab  30376  numclwlk2lem2f  30401  spansnid  31587  elspansn4  31597  fnpreimac  32698  ccatf1  32980  ccatws1f1olast  32983  swrdrn2  32985  swrdrn3  32986  swrdf1  32987  splfv3  32989  pwrssmgc  33031  wrdpmtrlast  33124  psgnfzto1stlem  33131  cycpmfv1  33144  cycpmfv2  33145  cycpmco2lem2  33158  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2  33164  cyc3co2  33171  cycpmrn  33174  submarchi  33217  subrdom  33316  fracfld  33339  imaslmod  33383  quslmod  33388  quslmhm  33389  nsgqusf1olem2  33444  lmhmqusker  33447  rhmquskerlem  33455  idlinsubrg  33461  drngidl  33463  rhmpreimaprmidl  33481  qsidomlem2  33483  mxidlprm  33500  opprmxidlabs  33517  qsdrngilem  33524  qsdrngi  33525  qsdrnglem2  33526  idlsrg0g  33536  pidufd  33573  dfufd2lem  33579  fply1  33588  evl1fpws  33594  ressply1evls1  33595  ressply1sub  33600  ply1asclunit  33604  r1plmhm  33640  extvfvcl  33650  evlextv  33656  mplvrpmga  33659  issply  33668  esplympl  33674  esplyind  33680  drgextlsp  33699  matdim  33721  ply1degltdimlem  33728  lindsunlem  33730  qusdimsum  33734  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  extdg1id  33772  evls1fldgencl  33776  irngss  33793  irngnzply1  33797  extdgfialglem1  33798  extdgfialglem2  33799  minplymindeg  33814  minplyirredlem  33816  irredminply  33822  algextdeglem2  33824  constrconj  33851  constrfiss  33857  1smat1  33910  submat1n  33911  lmatfval  33920  lmatcl  33922  mdetpmtr1  33929  madjusmdetlem4  33936  qtopt1  33941  qtophaus  33942  locfinref  33947  zarcls1  33975  zarclsiin  33977  zarmxt1  33986  zarcmplem  33987  rhmpreimacn  33991  ordtrest2NEWlem  34028  elzrhunit  34083  qqhcn  34097  qqhucn  34098  esumel  34153  esumsplit  34159  sigagenss2  34256  elsx  34300  sxbrsigalem0  34377  dya2icoseg  34383  eulerpartlemb  34474  eulerpartlemgvv  34482  iwrdsplit  34493  sseqfv2  34500  probfinmeasb  34534  dstrvprob  34578  dstfrvel  34580  ballotlemrv  34626  signstfvn  34675  signstfvp  34677  signstfveq0  34683  signsvtp  34689  signsvtn  34690  reprsuc  34721  reprpmtf1o  34732  lpadleft  34789  bnj1006  35065  bnj1018g  35068  bnj1018  35069  bnj1121  35090  bnj1398  35139  bnj1450  35155  bnj1501  35172  revpfxsfxrev  35259  swrdrevpfx  35260  pfxwlk  35267  revwlk  35268  swrdwlk  35270  subfacp1lem5  35327  ptpconn  35376  indispconn  35377  cvxsconn  35386  cvmseu  35419  cvmliftmolem2  35425  cvmliftlem7  35434  cvmliftlem10  35437  cvmliftlem13  35439  cvmlift2lem12  35457  satfv1lem  35505  satffunlem1lem2  35546  satffunlem2lem2  35549  satefvfmla1  35568  mrsubcv  35653  mrsubff  35655  mrsubrn  35656  mrsubccat  35661  elmrsubrn  35663  mrsubco  35664  mrsubvrs  35665  mvhf  35701  msubvrs  35703  mclsax  35712  r1peuqusdeg1  35786  linerflx1  36292  linerflx2  36294  fwddifnval  36306  elhf2  36318  neibastop2lem  36503  weiunpo  36608  weiunso  36609  icoreunrn  37503  relowlssretop  37507  sucneqond  37509  matunitlindflem2  37757  poimirlem4  37764  poimirlem20  37780  poimirlem30  37790  broucube  37794  opnmbllem0  37796  areacirclem2  37849  areacirclem4  37851  blssp  37896  sstotbnd2  37914  totbndbnd  37929  prdstotbnd  37934  cnpwstotbnd  37937  heiborlem9  37959  exidcl  38016  exidresid  38019  grpokerinj  38033  iscringd  38138  erimeq2  38876  prter3  39081  toycom  39172  islfld  39261  lshpsmreu  39308  ldualelvbase  39326  ldualssvscl  39357  lkreqN  39369  lkrlspeqN  39370  erng1lem  41186  erngdvlem4  41190  erng0g  41193  erng1r  41194  erngdvlem4-rN  41198  dva0g  41226  dia1dim2  41261  dia1dimid  41262  dia2dimlem5  41267  dvhelvbasei  41287  dvhvaddass  41296  tendoinvcl  41303  tendolinv  41304  tendorinv  41305  dvhgrp  41306  dvhlveclem  41307  cdlemn4  41397  lcfrlem12N  41753  lcfrlem15  41756  lcdvscl  41804  lcdlssvscl  41805  lcdvsass  41806  lcdvs0N  41815  mapdincl  41860  mapdin  41861  mapdlsmcl  41862  mapdcnvatN  41865  mapdpglem2  41872  mapdpglem12  41882  mapdpglem18  41888  mapdpglem21  41891  mapdpglem22  41892  mapdpglem28  41900  mapdpglem30  41901  hdmaprnlem3N  42049  hdmaprnlem3uN  42050  hdmaprnlem7N  42054  hdmaprnlem8N  42055  hdmaprnlem9N  42056  hdmaprnlem3eN  42057  hdmaprnlem16N  42061  hgmapdcl  42089  hgmapval1  42092  hgmaprnlem4N  42098  hdmapinvlem1  42117  fzadd2d  42171  aks6d1c2lem4  42320  sticksstones1  42339  sticksstones8  42346  sticksstones9  42347  sticksstones10  42348  sticksstones11  42349  sticksstones17  42356  sticksstones18  42357  aks6d1c6lem4  42366  rhmqusspan  42378  aks5lem2  42380  mhmcopsr  42744  evlsbagval  42754  evlsevl  42759  evlvvval  42760  evlvvvallem  42761  selvcllem2  42763  evlselv  42772  mhpind  42779  fltnltalem  42847  wepwsolem  43226  kercvrlsm  43267  dfacbasgrp  43292  onexomgt  43425  onexoegt  43428  onov0suclim  43458  cantnftermord  43504  cantnf2  43509  omcl2  43517  ofoaf  43539  ofoafo  43540  grurankcld  44416  grumnudlem  44468  grumnud  44469  inaex  44480  gruex  44481  dvconstbi  44517  cncmpmax  45219  iooabslt  45687  fmul01lt1lem2  45773  limciccioolb  45809  limcicciooub  45823  limsuppnfdlem  45887  climrescn  45934  climxrrelem  45935  climxrre  45936  liminflimsupxrre  46003  xlimmnfvlem2  46019  xlimpnfvlem2  46023  fsumcncf  46064  ioccncflimc  46071  icocncflimc  46075  cncfiooicclem1  46079  dvbdfbdioolem2  46115  dvnmul  46129  dvnprodlem1  46132  stoweidlem26  46212  stoweidlem34  46220  stoweidlem48  46234  stoweidlem59  46245  dirkercncflem3  46291  fourierdlem32  46325  fourierdlem41  46334  fourierdlem51  46343  fourierdlem63  46355  fourierdlem82  46374  fourierdlem85  46377  fourierdlem93  46385  fourierdlem111  46403  fourierdlem114  46406  etransclem35  46455  hspdifhsp  46802  opnvonmbllem1  46818  ovnovollem1  46842  mbfresmf  46925  smfaddlem1  46949  smfsuplem1  46997  smflimsuplem5  47010  chnerlem2  47069  setsidel  47564  setsnidel  47565  imasetpreimafvbijlemf  47589  prelspr  47674  upgrimpths  48097  gpgprismgr4cycllem9  48291  rngccatidALTV  48460  rhmsubcALTVlem3  48471  funcringcsetcALTV2lem3  48480  funcringcsetcALTV2lem8  48485  ringccatidALTV  48494  funcringcsetclem3ALTV  48503  funcringcsetclem8ALTV  48508  srhmsubcALTVlem1  48511  srhmsubcALTV  48513  lcosslsp  48626  nnolog2flm1  48778  ffvbr  49043  glbprlem  49152  topdlat  49191  catprs  49198  iinfsubc  49245  iinfconstbaslem  49252  imaid  49341  fthcomf  49344  uptr2  49408  natoppf2  49417  natoppfb  49418  swapf2  49461  swapfiso  49472  swapciso  49473  oppc1stflem  49474  cofuswapf2  49482  fuco22natlem  49532  fucoppcffth  49598  oppcthinco  49626  oppcthinendcALT  49628  thinccisod  49641  termco  49668  termchommo  49672  termcid  49673  termcterm  49700  termcterm2  49701  diagciso  49726  diagcic  49727  funcsn  49728  uobeqterm  49733  mndtccatid  49774  grptcmon  49780  grptcepi  49781  2arwcat  49787  lanval2  49814  ranval2  49817  lanup  49828  ranup  49829  lmddu  49854