Theorem eleqtrrd 2918

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

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

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  3eltr4d  2930  rspc2vd  3934  disjxiun  5065  eldmressnsn  5897  elimdelov  7252  elovmpt3rab1  7407  fnwelem  7827  tfrlem13  8028  tz7.44-2  8045  omordi  8194  oneo  8209  omeulem2  8211  oeordi  8215  oeeui  8230  nnneo  8280  erref  8311  en1uniel  8583  omxpenlem  8620  unblem3  8774  dffi3  8897  ordtypelem10  8993  oismo  9006  cantnff  9139  cantnfp1lem3  9145  cantnflem1  9154  cnfcom  9165  r1ordg  9209  r1pwss  9215  rankwflemb  9224  r1elwf  9227  rankidb  9231  rankonidlem  9259  fseqenlem2  9453  dfac12lem1  9571  dfac12lem2  9572  pwsdompw  9628  ackbij2lem3  9665  ackbij2  9667  cfsmolem  9694  hsmexlem4  9853  ttukeylem3  9935  ttukeylem7  9939  iundom2g  9964  fpwwe2lem9  10062  canthwelem  10074  pwfseqlem4  10086  winalim2  10120  r1wunlim  10161  tskmid  10264  fzopth  12947  predfz  13035  fzoss2  13068  fz1fzo0m1  13088  fzo0addel  13094  fzo0addelr  13095  fzosubel3  13101  elfzomin  13112  elfzonlteqm1  13116  fzoend  13131  fzofzp1  13137  fzofzp1b  13138  peano2fzor  13147  zmodfzo  13265  seqf1olem2  13413  bcn2  13682  swrdccat2  14033  pfxccat1  14066  swrdswrd  14069  pfxccatin12  14097  splfv1  14119  revcl  14125  revlen  14126  revccat  14130  revrev  14131  repswpfx  14149  cshwidxmod  14167  revco  14198  limsupgre  14840  summolem2a  15074  fsumm1  15108  fsumcom2  15131  prodmolem2a  15290  fprodm1  15323  fprodcom2  15340  prmreclem4  16257  prmreclem5  16258  vdwapid1  16313  vdwlem5  16323  vdwlem8  16326  vdwnnlem2  16334  ramub1lem1  16364  ramub1lem2  16365  mrieqvlemd  16902  mreexd  16915  mreexexlemd  16917  catcocl  16958  catass  16959  moni  17008  epii  17015  inviso1  17038  episect  17057  invisoinvl  17062  catsubcat  17111  subccocl  17117  fullsubc  17122  funcco  17143  resf2nd  17167  funcres  17168  fthepi  17200  nati  17227  arwhoma  17307  catccatid  17364  resscatc  17367  catcisolem  17368  catcoppccl  17370  catcfuccl  17371  estrreslem2  17390  funcestrcsetclem3  17394  funcestrcsetclem8  17399  equivestrcsetc  17404  funcsetcestrclem3  17408  funcsetcestrclem8  17414  xpcco  17435  xpcco2  17439  xpccatid  17440  prfcl  17455  catcxpccl  17459  curf12  17479  curf1cl  17480  curf2  17481  curf2cl  17483  curfcl  17484  uncf2  17489  uncfcurf  17491  diag12  17496  diag2  17497  curf2ndf  17499  hofcl  17511  oppchofcl  17512  oyoncl  17522  yonedalem3a  17526  yonedalem4b  17528  yonedalem22  17530  yonedalem3b  17531  yonedalem3  17532  yonedainv  17533  yonffthlem  17534  latcl2  17660  latlem  17661  latjcom  17671  latmcom  17687  clatlem  17723  clatlubcl2  17725  clatglbcl2  17727  acsfiindd  17789  gsumpropd2lem  17891  mndpropd  17938  imasmnd  17951  frmdmnd  18026  frmdgsum  18029  grpsubpropd2  18207  imasgrp  18217  subg0  18287  0ghm  18374  resghm2  18377  ghmco  18380  pwsdiagghm  18388  psgnunilem1  18623  psgnunilem5  18624  psgnunilem2  18625  psgnunilem3  18626  sylow1lem4  18728  sylow1lem5  18729  efglem  18844  efgtf  18850  efginvrel2  18855  efginvrel1  18856  efgsdmi  18860  efgs1b  18864  efgsres  18866  efgsfo  18867  efgredleme  18871  efgredlemc  18873  efgredlem  18875  efgcpbllemb  18883  frgp0  18888  frgpadd  18891  frgpinv  18892  vrgpf  18896  vrgpinv  18897  frgpuplem  18900  frgpup1  18903  frgpup2  18904  frgpup3lem  18905  frgpnabllem1  18995  frgpnabllem2  18996  gsumval3  19029  dprdfid  19141  dprdsn  19160  dprd2da  19166  dpjidcl  19182  pgpfac1lem2  19199  pgpfaclem3  19207  ablsimpg1gend  19229  ablsimpgprmd  19239  ringpropd  19334  imasring  19371  qusring2  19372  pwsco1rhm  19492  pwsco2rhm  19493  subrgunit  19555  pwsdiagrhm  19571  cntzsdrg  19583  isabvd  19593  lmodprop2d  19698  islssd  19709  prdsvscacl  19742  prdslmodd  19743  islmhm2  19812  lmhmco  19817  lmhmplusg  19818  lmhmvsca  19819  lmhmpropd  19847  lsppreli  19864  lspsnel4  19898  lssacsex  19918  lspsnat  19919  qus1  20010  qusrhm  20012  assapropd  20103  psr0cl  20176  psrnegcl  20178  psr1cl  20184  resspsrmul  20199  subrgpsr  20201  mvrf  20206  mplmon  20246  mplcoe1  20248  subrgasclcl  20281  mplind  20284  evlslem1  20297  subrgply1  20403  psrplusgpropd  20406  ply1coe  20466  cply1coe0bi  20470  lply1binomsc  20477  evls1val  20485  evls1rhm  20487  evl1val  20494  evl1rhm  20497  pf1ind  20520  evl1scvarpw  20528  znf1o  20700  cssmre  20839  dsmmlss  20890  frlmsplit2  20919  frlmbas3  20922  frlmup1  20944  matbas2i  21033  matplusg2  21038  matvsca2  21039  matsubgcell  21045  matvscacell  21047  mpomatmul  21057  mavmulval  21156  mavmulcl  21158  mavmulass  21160  mavmul0  21163  mavmumamul1  21166  m1detdiag  21208  cramerimplem2  21295  mat2pmatmul  21341  mat2pmatlin  21345  monmatcollpw  21389  pmatcollpwfi  21392  mply1topmatcl  21415  pm2mpghm  21426  pm2mpmhmlem2  21429  pm2mp  21435  chpmat1dlem  21445  chpmat1d  21446  chpdmatlem0  21447  chpscmat  21452  chpscmatgsumbin  21454  chpscmatgsummon  21455  chfacfscmulcl  21467  cpmadugsumlemB  21484  cpmadugsumlemC  21485  chcoeffeqlem  21495  cldmreon  21704  neiptopreu  21743  maxlp  21757  ordttopon  21803  ordtrest2lem  21813  cnprcl2  21861  lmcnp  21914  resthauslem  21973  hauscmplem  22016  1stcfb  22055  2ndcctbss  22065  2ndcomap  22068  dis2ndc  22070  loclly  22097  hausllycmp  22104  locfincmp  22136  dissnref  22138  kgeni  22147  kgenidm  22157  ptpjpre2  22190  xkoopn  22199  txopn  22212  ptpjopn  22222  ptcldmpt  22224  ptcls  22226  pthaus  22248  txkgen  22262  xkohaus  22263  xkopt  22265  txconn  22299  imastps  22331  kqid  22338  kqopn  22344  kqcld  22345  isr0  22347  indishmph  22408  pt1hmeo  22416  ptuncnv  22417  ptunhmeo  22418  t0kq  22428  filconn  22493  uzrest  22507  uffixsn  22535  fmfnfmlem2  22565  flimss2  22582  flimss1  22583  flimclslem  22594  flfcnp  22614  fclsfnflim  22637  uffclsflim  22641  fcfelbas  22646  alexsublem  22654  alexsub  22655  cnextcn  22677  cnextfres1  22678  cnextfres  22679  tmdgsum  22705  distgp  22709  indistgp  22710  symgtgp  22716  ghmcnp  22725  qustgpopn  22730  qustgplem  22731  qustgphaus  22733  prdstmdd  22734  prdstgpd  22735  tsmsid  22750  tsmssubm  22753  tsmsmhm  22756  tsmsadd  22757  tsmssplit  22762  utop2nei  22861  utop3cls  22862  neipcfilu  22907  cnextucn  22914  ucnextcn  22915  blpnfctr  23048  lpbl  23115  met2ndci  23134  tmsxps  23148  metcnpi  23156  metcnpi2  23157  metcnpi3  23158  metustid  23166  metustsym  23167  metustexhalf  23168  subgngp  23246  ngptgp  23247  sranlm  23295  nlmvscn  23298  nrginvrcn  23303  lssnlm  23312  nghmcn  23356  iccntr  23431  icccmplem2  23433  msdcn  23451  cncfmptc  23521  cncfmptid  23522  cncfmpt2f  23524  icoopnst  23545  iocopnst  23546  nmoleub2lem3  23721  nmoleub3  23725  nmhmcn  23726  ipcn  23851  cfilfcls  23879  caucfil  23888  equivcau  23905  caubl  23913  flimcfil  23919  cmssmscld  23955  rrxdstprj1  24014  minveclem3b  24033  minveclem4  24037  ovolicc2lem3  24122  ovolicc2lem4  24123  opnmbllem  24204  vitalilem2  24212  mbfsup  24267  mbfinf  24268  mbfi1fseqlem4  24321  limccnp  24491  limccnp2  24492  dvreslem  24509  dvres2lem  24510  dvidlem  24515  dvcnp2  24519  dvcn  24520  dvaddbr  24537  dvmulbr  24538  dvcmul  24543  dvcof  24547  dvcnvlem  24575  dvef  24579  rollelem  24588  dvlip2  24594  dvivthlem1  24607  dvivth  24609  lhop2  24614  lhop  24615  dvcnvrelem1  24616  dvcnvrelem2  24617  dvcnvre  24618  ply1rem  24759  fta1blem  24764  plycpn  24880  plyrem  24896  tayl0  24952  dvtaylp  24960  dvntaylp  24961  dvntaylp0  24962  taylthlem1  24963  taylthlem2  24964  ulmdvlem3  24992  psercn  25016  pserdv  25019  abelth  25031  efabl  25136  efopnlem1  25241  loglesqrt  25341  relogbf  25371  efrlim  25549  dchrghm  25834  dchrptlem3  25844  tgbtwntriv2  26275  tgbtwnne  26278  ercgrg  26305  tgidinside  26359  tgbtwnconn1  26363  tglnne  26416  tglnne0  26428  tglnpt2  26429  tglineneq  26432  ncolncol  26434  coltr3  26436  mirln  26464  mirln2  26465  mirconn  26466  krippenlem  26478  footexALT  26506  footexlem1  26507  footexlem2  26508  colperpexlem3  26520  mideulem2  26522  opphllem  26523  oppne3  26531  opphllem1  26535  opphllem2  26536  opphllem4  26538  oppperpex  26541  opphl  26542  hlpasch  26544  hpgerlem  26553  colhp  26558  midbtwn  26567  lmieu  26572  lmiisolem  26584  sacgr  26619  f1otrg  26659  f1otrge  26660  ebtwntg  26770  ecgrtg  26771  eengtrkg  26774  eengtrkge  26775  upgr1eop  26902  usgredg3  27000  uspgr1eop  27031  usgr1eop  27034  vtxdun  27265  vtxdfiun  27266  1loopgruspgr  27284  1loopgrvd2  27287  1hevtxdg1  27290  1egrvtxdg1  27293  1egrvtxdg0  27295  umgr2v2e  27309  wlkres  27454  wlkp1lem4  27460  wlkp1  27465  wwlksm1edg  27661  wwlksnext  27673  wwlksnextproplem3  27692  clwwlkel  27827  1wlkdlem2  27919  trlsegvdeg  28008  eupth2lem3lem1  28009  eupth2lem3lem2  28010  extwwlkfab  28133  numclwlk2lem2f  28158  spansnid  29342  elspansn4  29352  fnpreimac  30418  ccatf1  30627  swrdrn2  30630  swrdrn3  30631  swrdf1  30632  splfv3  30634  psgnfzto1stlem  30744  cycpmfv1  30757  cycpmfv2  30758  cycpmco2lem2  30771  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2  30777  cyc3co2  30784  cycpmrn  30787  submarchi  30817  imaslmod  30924  quslmod  30925  quslmhm  30926  fply1  30933  lidlnsg  30963  qsidomlem2  30968  mxidlprm  30979  drgextlsp  30998  matdim  31015  lindsunlem  31022  qusdimsum  31026  fedgmullem1  31027  fedgmullem2  31028  fedgmul  31029  extdg1id  31055  1smat1  31071  submat1n  31072  lmatfval  31081  lmatcl  31083  mdetpmtr1  31090  madjusmdetlem4  31097  qtopt1  31101  qtophaus  31102  locfinref  31107  ordtrest2NEWlem  31167  elzrhunit  31222  qqhcn  31234  qqhucn  31235  esumel  31308  esumsplit  31314  sigagenss2  31411  elsx  31455  sxbrsigalem0  31531  dya2icoseg  31537  eulerpartlemb  31628  eulerpartlemgvv  31636  iwrdsplit  31647  sseqfv2  31654  probfinmeasb  31688  dstrvprob  31731  dstfrvel  31733  ballotlemrv  31779  signstfvn  31841  signstfvp  31843  signstfveq0  31849  signsvtp  31855  signsvtn  31856  reprsuc  31888  reprpmtf1o  31899  lpadleft  31956  bnj1006  32234  bnj1018g  32237  bnj1018  32238  bnj1121  32259  bnj1398  32308  bnj1450  32324  bnj1501  32341  revpfxsfxrev  32364  swrdrevpfx  32365  pfxwlk  32372  revwlk  32373  swrdwlk  32375  subfacp1lem5  32433  ptpconn  32482  indispconn  32483  cvxsconn  32492  cvmseu  32525  cvmliftmolem2  32531  cvmliftlem7  32540  cvmliftlem10  32543  cvmliftlem13  32545  cvmlift2lem12  32563  satfv1lem  32611  satffunlem1lem2  32652  satffunlem2lem2  32655  satefvfmla1  32674  mrsubcv  32759  mrsubff  32761  mrsubrn  32762  mrsubccat  32767  elmrsubrn  32769  mrsubco  32770  mrsubvrs  32771  mvhf  32807  msubvrs  32809  mclsax  32818  nodenselem5  33194  nosupres  33209  linerflx1  33612  linerflx2  33614  fwddifnval  33626  elhf2  33638  neibastop2lem  33710  icoreunrn  34642  relowlssretop  34646  sucneqond  34648  matunitlindflem2  34891  poimirlem4  34898  poimirlem20  34914  poimirlem30  34924  broucube  34928  opnmbllem0  34930  areacirclem2  34985  areacirclem4  34987  blssp  35033  sstotbnd2  35054  totbndbnd  35069  prdstotbnd  35074  cnpwstotbnd  35077  heiborlem9  35099  exidcl  35156  exidresid  35159  grpokerinj  35173  iscringd  35278  erim2  35913  prter3  36020  toycom  36111  islfld  36200  lshpsmreu  36247  ldualelvbase  36265  ldualssvscl  36296  lkreqN  36308  lkrlspeqN  36309  erng1lem  38125  erngdvlem4  38129  erng0g  38132  erng1r  38133  erngdvlem4-rN  38137  dva0g  38165  dia1dim2  38200  dia1dimid  38201  dia2dimlem5  38206  dvhelvbasei  38226  dvhvaddass  38235  tendoinvcl  38242  tendolinv  38243  tendorinv  38244  dvhgrp  38245  dvhlveclem  38246  cdlemn4  38336  lcfrlem12N  38692  lcfrlem15  38695  lcdvscl  38743  lcdlssvscl  38744  lcdvsass  38745  lcdvs0N  38754  mapdincl  38799  mapdin  38800  mapdlsmcl  38801  mapdcnvatN  38804  mapdpglem2  38811  mapdpglem12  38821  mapdpglem18  38827  mapdpglem21  38830  mapdpglem22  38831  mapdpglem28  38839  mapdpglem30  38840  hdmaprnlem3N  38988  hdmaprnlem3uN  38989  hdmaprnlem7N  38993  hdmaprnlem8N  38994  hdmaprnlem9N  38995  hdmaprnlem3eN  38996  hdmaprnlem16N  39000  hgmapdcl  39028  hgmapval1  39031  hgmaprnlem4N  39037  hdmapinvlem1  39056  fnsnbt  39127  selvval2lem2  39140  selvval2lem4  39143  fltnltalem  39281  wepwsolem  39649  kercvrlsm  39690  dfacbasgrp  39715  imo72b2lem0  40523  grurankcld  40576  grumnudlem  40628  grumnud  40629  inaex  40640  gruex  40641  dvconstbi  40673  cncmpmax  41296  iooabslt  41781  fmul01lt1lem2  41873  limciccioolb  41909  limcicciooub  41925  limsuppnfdlem  41989  climrescn  42036  climxrrelem  42037  climxrre  42038  liminflimsupxrre  42105  xlimmnfvlem2  42121  xlimpnfvlem2  42125  fsumcncf  42168  ioccncflimc  42175  icocncflimc  42179  cncfiooicclem1  42183  dvbdfbdioolem2  42221  dvnmul  42235  stoweidlem26  42318  stoweidlem34  42326  stoweidlem48  42340  stoweidlem59  42351  dirkercncflem3  42397  fourierdlem32  42431  fourierdlem41  42440  fourierdlem51  42449  fourierdlem63  42461  fourierdlem82  42480  fourierdlem85  42483  fourierdlem93  42491  fourierdlem111  42509  fourierdlem114  42512  etransclem35  42561  hspdifhsp  42905  opnvonmbllem1  42921  ovnovollem1  42945  mbfresmf  43023  smfaddlem1  43046  smfsuplem1  43092  smflimsuplem5  43105  fzoopth  43534  setsidel  43543  setsnidel  43544  imasetpreimafvbijlemf  43568  prelspr  43655  rnghmsubcsetclem1  44253  rngccatidALTV  44267  zrinitorngc  44278  zrtermorngc  44279  zrzeroorngc  44280  rhmsubcsetclem1  44299  rhmsubcrngclem1  44305  funcringcsetcALTV2lem3  44316  funcringcsetcALTV2lem8  44321  ringccatidALTV  44330  funcringcsetclem3ALTV  44339  funcringcsetclem8ALTV  44344  irinitoringc  44347  zrtermoringc  44348  zrninitoringc  44349  nzerooringczr  44350  srhmsubclem2  44352  srhmsubc  44354  srhmsubcALTVlem1  44370  srhmsubcALTV  44372  rhmsubcALTVlem3  44384  lcosslsp  44500  nnolog2flm1  44657