Theorem eleqtrrd 2834

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  3eltr4d  2846  rspc2vd  3943  disjxiun  5144  eldmressnsn  6023  elimdelov  7507  elovmpt3rab1  7668  fnwelem  8119  tfrlem13  8392  tz7.44-2  8409  omordi  8568  oneo  8583  omeulem2  8585  oeordi  8589  oeeui  8604  nnneo  8656  naddelim  8687  erref  8725  en1uniel  9030  en1unielOLD  9031  omxpenlem  9075  unblem3  9299  dffi3  9428  ordtypelem10  9524  oismo  9537  cantnff  9671  cantnfp1lem3  9677  cantnflem1  9686  cnfcom  9697  r1ordg  9775  r1pwss  9781  rankwflemb  9790  r1elwf  9793  rankidb  9797  rankonidlem  9825  fseqenlem2  10022  dfac12lem1  10140  dfac12lem2  10141  pwsdompw  10201  ackbij2lem3  10238  ackbij2  10240  cfsmolem  10267  hsmexlem4  10426  ttukeylem3  10508  ttukeylem7  10512  iundom2g  10537  fpwwe2lem8  10635  canthwelem  10647  pwfseqlem4  10659  winalim2  10693  r1wunlim  10734  tskmid  10837  fzopth  13542  predfz  13630  fzoss2  13664  fz1fzo0m1  13684  fzo0addel  13690  fzo0addelr  13691  fzosubel3  13697  elfzomin  13708  elfzonlteqm1  13712  fzoend  13727  fzofzp1  13733  fzofzp1b  13734  peano2fzor  13743  zmodfzo  13863  seqf1olem2  14012  bcn2  14283  swrdccat2  14623  pfxccat1  14656  swrdswrd  14659  pfxccatin12  14687  splfv1  14709  revcl  14715  revlen  14716  revccat  14720  revrev  14721  repswpfx  14739  cshwidxmod  14757  revco  14789  limsupgre  15429  summolem2a  15665  fsumm1  15701  fsumcom2  15724  prodmolem2a  15882  fprodm1  15915  fprodcom2  15932  prmreclem4  16856  prmreclem5  16857  vdwapid1  16912  vdwlem5  16922  vdwlem8  16925  vdwnnlem2  16933  ramub1lem1  16963  ramub1lem2  16964  mrieqvlemd  17577  mreexd  17590  mreexexlemd  17592  catcocl  17633  catass  17634  moni  17687  epii  17694  inviso1  17717  episect  17736  invisoinvl  17741  catsubcat  17793  subccocl  17799  fullsubc  17804  funcco  17825  resf2nd  17849  funcres  17850  fthepi  17883  nati  17910  arwhoma  17999  catccatid  18060  resscatc  18063  catcisolem  18064  catcoppccl  18071  catcoppcclOLD  18072  catcfuccl  18073  catcfucclOLD  18074  estrreslem2  18094  funcestrcsetclem3  18098  funcestrcsetclem8  18103  equivestrcsetc  18108  funcsetcestrclem3  18112  funcsetcestrclem8  18118  xpcco  18139  xpcco2  18143  xpccatid  18144  prfcl  18159  catcxpccl  18163  catcxpcclOLD  18164  curf12  18184  curf1cl  18185  curf2  18186  curf2cl  18188  curfcl  18189  uncf2  18194  uncfcurf  18196  diag12  18201  diag2  18202  curf2ndf  18204  hofcl  18216  oppchofcl  18217  oyoncl  18227  yonedalem3a  18231  yonedalem4b  18233  yonedalem22  18235  yonedalem3b  18236  yonedalem3  18237  yonedainv  18238  yonffthlem  18239  latcl2  18393  latlem  18394  latjcom  18404  latmcom  18420  clatlem  18459  clatlubcl2  18461  clatglbcl2  18463  acsfiindd  18510  gsumpropd2lem  18604  sgrppropd  18656  mndpropd  18684  imasmnd  18697  frmdmnd  18776  frmdgsum  18779  grpsubpropd2  18965  imasgrp  18975  subg0  19048  0ghm  19144  resghm2  19147  ghmco  19150  pwsdiagghm  19158  psgnunilem1  19402  psgnunilem5  19403  psgnunilem2  19404  psgnunilem3  19405  sylow1lem4  19510  sylow1lem5  19511  efglem  19625  efgtf  19631  efginvrel2  19636  efginvrel1  19637  efgsdmi  19641  efgs1b  19645  efgsres  19647  efgsfo  19648  efgredleme  19652  efgredlemc  19654  efgredlem  19656  efgcpbllemb  19664  frgp0  19669  frgpadd  19672  frgpinv  19673  vrgpf  19677  vrgpinv  19678  frgpuplem  19681  frgpup1  19684  frgpup2  19685  frgpup3lem  19686  frgpnabllem1  19782  frgpnabllem2  19783  gsumval3  19816  dprdfid  19928  dprdsn  19947  dprd2da  19953  dpjidcl  19969  pgpfac1lem2  19986  pgpfaclem3  19994  ablsimpg1gend  20016  ablsimpgprmd  20026  rngpropd  20068  imasrng  20071  ringpropd  20176  imasring  20218  qusring2  20222  pwsco1rhm  20393  pwsco2rhm  20394  lringuplu  20432  subrgunit  20480  pwsdiagrhm  20497  cntzsdrg  20561  isabvd  20571  lmodprop2d  20678  islssd  20690  prdsvscacl  20723  prdslmodd  20724  islmhm2  20793  lmhmco  20798  lmhmplusg  20799  lmhmvsca  20800  lmhmpropd  20828  lsppreli  20845  lspsnel4  20882  lssacsex  20902  lspsnat  20903  qus1  21022  qusrhm  21024  qus2idrng  21044  rngqiprngghmlem1  21046  rngqiprngfulem1  21070  znf1o  21326  cssmre  21465  dsmmlss  21518  frlmsplit2  21547  frlmbas3  21550  frlmup1  21572  assapropd  21645  psr0cl  21732  psrnegcl  21734  psr1cl  21741  resspsrmul  21756  subrgpsr  21758  mvrf  21763  mplmon  21809  mplcoe1  21811  subrgasclcl  21847  mplind  21850  evlslem1  21864  subrgply1  21975  psrplusgpropd  21978  ply1coe  22040  cply1coe0bi  22044  lply1binomsc  22051  evls1val  22059  evls1rhm  22061  evl1val  22068  evl1rhm  22071  pf1ind  22094  evl1scvarpw  22102  matbas2i  22144  matplusg2  22149  matvsca2  22150  matsubgcell  22156  matvscacell  22158  mpomatmul  22168  mavmulval  22267  mavmulcl  22269  mavmulass  22271  mavmul0  22274  mavmumamul1  22277  m1detdiag  22319  cramerimplem2  22406  mat2pmatmul  22453  mat2pmatlin  22457  monmatcollpw  22501  pmatcollpwfi  22504  mply1topmatcl  22527  pm2mpghm  22538  pm2mpmhmlem2  22541  pm2mp  22547  chpmat1dlem  22557  chpmat1d  22558  chpdmatlem0  22559  chpscmat  22564  chpscmatgsumbin  22566  chpscmatgsummon  22567  chfacfscmulcl  22579  cpmadugsumlemB  22596  cpmadugsumlemC  22597  chcoeffeqlem  22607  cldmreon  22818  neiptopreu  22857  maxlp  22871  ordttopon  22917  ordtrest2lem  22927  cnprcl2  22975  lmcnp  23028  resthauslem  23087  hauscmplem  23130  1stcfb  23169  2ndcctbss  23179  2ndcomap  23182  dis2ndc  23184  loclly  23211  hausllycmp  23218  locfincmp  23250  dissnref  23252  kgeni  23261  kgenidm  23271  ptpjpre2  23304  xkoopn  23313  txopn  23326  ptpjopn  23336  ptcldmpt  23338  ptcls  23340  pthaus  23362  txkgen  23376  xkohaus  23377  xkopt  23379  txconn  23413  imastps  23445  kqid  23452  kqopn  23458  kqcld  23459  isr0  23461  indishmph  23522  pt1hmeo  23530  ptuncnv  23531  ptunhmeo  23532  t0kq  23542  filconn  23607  uzrest  23621  uffixsn  23649  fmfnfmlem2  23679  flimss2  23696  flimss1  23697  flimclslem  23708  flfcnp  23728  fclsfnflim  23751  uffclsflim  23755  fcfelbas  23760  alexsublem  23768  alexsub  23769  cnextcn  23791  cnextfres1  23792  cnextfres  23793  tmdgsum  23819  distgp  23823  indistgp  23824  symgtgp  23830  ghmcnp  23839  qustgpopn  23844  qustgplem  23845  qustgphaus  23847  prdstmdd  23848  prdstgpd  23849  tsmsid  23864  tsmssubm  23867  tsmsmhm  23870  tsmsadd  23871  tsmssplit  23876  utop2nei  23975  utop3cls  23976  neipcfilu  24021  cnextucn  24028  ucnextcn  24029  blpnfctr  24162  lpbl  24232  met2ndci  24251  tmsxps  24265  metcnpi  24273  metcnpi2  24274  metcnpi3  24275  metustid  24283  metustsym  24284  metustexhalf  24285  subgngp  24364  ngptgp  24365  sranlm  24421  nlmvscn  24424  nrginvrcn  24429  lssnlm  24438  nghmcn  24482  iccntr  24557  icccmplem2  24559  msdcn  24577  cncfmptc  24652  cncfmptid  24653  cncfmpt2f  24655  icoopnst  24683  iocopnst  24684  nmoleub2lem3  24862  nmoleub3  24866  nmhmcn  24867  ipcn  24994  cfilfcls  25022  caucfil  25031  equivcau  25048  caubl  25056  flimcfil  25062  cmssmscld  25098  rrxdstprj1  25157  minveclem3b  25176  minveclem4  25180  mulcncf  25194  ovolicc2lem3  25268  ovolicc2lem4  25269  opnmbllem  25350  vitalilem2  25358  mbfsup  25413  mbfinf  25414  mbfi1fseqlem4  25468  limccnp  25640  limccnp2  25641  dvreslem  25658  dvres2lem  25659  dvidlem  25664  dvcnp2  25669  dvcnp2OLD  25670  dvcn  25671  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcmul  25695  dvcof  25700  dvcnvlem  25728  dvef  25732  rollelem  25741  dvlip2  25747  dvivthlem1  25760  dvivth  25762  lhop2  25767  lhop  25768  dvcnvrelem1  25769  dvcnvrelem2  25770  dvcnvre  25771  ply1rem  25916  fta1blem  25921  plycpn  26038  plyrem  26054  tayl0  26110  dvtaylp  26118  dvntaylp  26119  dvntaylp0  26120  taylthlem1  26121  taylthlem2  26122  ulmdvlem3  26150  psercn  26174  pserdv  26177  abelth  26189  efabl  26295  efopnlem1  26400  loglesqrt  26502  relogbf  26532  efrlim  26710  dchrghm  26995  dchrptlem3  27005  nodenselem5  27427  nosupres  27446  noinfres  27461  sltlpss  27638  precsexlem11  27902  tgbtwntriv2  28005  tgbtwnne  28008  ercgrg  28035  tgidinside  28089  tgbtwnconn1  28093  tglnne  28146  tglnne0  28158  tglnpt2  28159  tglineneq  28162  ncolncol  28164  coltr3  28166  mirln  28194  mirln2  28195  mirconn  28196  krippenlem  28208  footexALT  28236  footexlem1  28237  footexlem2  28238  colperpexlem3  28250  mideulem2  28252  opphllem  28253  oppne3  28261  opphllem1  28265  opphllem2  28266  opphllem4  28268  oppperpex  28271  opphl  28272  hlpasch  28274  hpgerlem  28283  colhp  28288  midbtwn  28297  lmieu  28302  lmiisolem  28314  sacgr  28349  f1otrg  28389  f1otrge  28390  ebtwntg  28507  ecgrtg  28508  eengtrkg  28511  eengtrkge  28512  upgr1eop  28642  usgredg3  28740  uspgr1eop  28771  usgr1eop  28774  vtxdun  29005  vtxdfiun  29006  1loopgruspgr  29024  1loopgrvd2  29027  1hevtxdg1  29030  1egrvtxdg1  29033  1egrvtxdg0  29035  umgr2v2e  29049  wlkres  29194  wlkp1lem4  29200  wlkp1  29205  wwlksm1edg  29402  wwlksnext  29414  wwlksnextproplem3  29432  clwwlkel  29566  1wlkdlem2  29658  trlsegvdeg  29747  eupth2lem3lem1  29748  eupth2lem3lem2  29749  extwwlkfab  29872  numclwlk2lem2f  29897  spansnid  31083  elspansn4  31093  fnpreimac  32163  ccatf1  32382  swrdrn2  32385  swrdrn3  32386  swrdf1  32387  splfv3  32389  pwrssmgc  32437  psgnfzto1stlem  32529  cycpmfv1  32542  cycpmfv2  32543  cycpmco2lem2  32556  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2  32562  cyc3co2  32569  cycpmrn  32572  submarchi  32602  imaslmod  32738  quslmod  32743  quslmhm  32744  nsgqusf1olem2  32799  ghmquskerlem2  32804  ghmquskerlem3  32805  ghmqusker  32806  lmhmqusker  32808  rhmpreimaidl  32811  rhmquskerlem  32817  idlinsubrg  32823  drngidl  32825  lidlnsg  32838  rhmpreimaprmidl  32844  qsidomlem2  32846  mxidlprm  32860  opprmxidlabs  32875  qsdrngilem  32882  qsdrngi  32883  qsdrnglem2  32884  idlsrg0g  32894  fply1  32911  evls1fpws  32920  ply1asclunit  32928  ressply1sub  32933  ply1fermltlchr  32936  r1plmhm  32955  drgextlsp  32968  matdim  32988  ply1degltdimlem  32995  lindsunlem  32997  qusdimsum  33001  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  extdg1id  33030  evls1fldgencl  33033  irngss  33040  irngnzply1  33044  minplyirredlem  33058  algextdeglem2  33063  1smat1  33082  submat1n  33083  lmatfval  33092  lmatcl  33094  mdetpmtr1  33101  madjusmdetlem4  33108  qtopt1  33113  qtophaus  33114  locfinref  33119  zarcls1  33147  zarclsiin  33149  zarmxt1  33158  zarcmplem  33159  rhmpreimacn  33163  ordtrest2NEWlem  33200  elzrhunit  33257  qqhcn  33269  qqhucn  33270  esumel  33343  esumsplit  33349  sigagenss2  33446  elsx  33490  sxbrsigalem0  33568  dya2icoseg  33574  eulerpartlemb  33665  eulerpartlemgvv  33673  iwrdsplit  33684  sseqfv2  33691  probfinmeasb  33725  dstrvprob  33768  dstfrvel  33770  ballotlemrv  33816  signstfvn  33878  signstfvp  33880  signstfveq0  33886  signsvtp  33892  signsvtn  33893  reprsuc  33925  reprpmtf1o  33936  lpadleft  33993  bnj1006  34269  bnj1018g  34272  bnj1018  34273  bnj1121  34294  bnj1398  34343  bnj1450  34359  bnj1501  34376  revpfxsfxrev  34404  swrdrevpfx  34405  pfxwlk  34412  revwlk  34413  swrdwlk  34415  subfacp1lem5  34473  ptpconn  34522  indispconn  34523  cvxsconn  34532  cvmseu  34565  cvmliftmolem2  34571  cvmliftlem7  34580  cvmliftlem10  34583  cvmliftlem13  34585  cvmlift2lem12  34603  satfv1lem  34651  satffunlem1lem2  34692  satffunlem2lem2  34695  satefvfmla1  34714  mrsubcv  34799  mrsubff  34801  mrsubrn  34802  mrsubccat  34807  elmrsubrn  34809  mrsubco  34810  mrsubvrs  34811  mvhf  34847  msubvrs  34849  mclsax  34858  linerflx1  35425  linerflx2  35427  fwddifnval  35439  elhf2  35451  neibastop2lem  35548  icoreunrn  36543  relowlssretop  36547  sucneqond  36549  matunitlindflem2  36788  poimirlem4  36795  poimirlem20  36811  poimirlem30  36821  broucube  36825  opnmbllem0  36827  areacirclem2  36880  areacirclem4  36882  blssp  36927  sstotbnd2  36945  totbndbnd  36960  prdstotbnd  36965  cnpwstotbnd  36968  heiborlem9  36990  exidcl  37047  exidresid  37050  grpokerinj  37064  iscringd  37169  erimeq2  37851  prter3  38055  toycom  38146  islfld  38235  lshpsmreu  38282  ldualelvbase  38300  ldualssvscl  38331  lkreqN  38343  lkrlspeqN  38344  erng1lem  40161  erngdvlem4  40165  erng0g  40168  erng1r  40169  erngdvlem4-rN  40173  dva0g  40201  dia1dim2  40236  dia1dimid  40237  dia2dimlem5  40242  dvhelvbasei  40262  dvhvaddass  40271  tendoinvcl  40278  tendolinv  40279  tendorinv  40280  dvhgrp  40281  dvhlveclem  40282  cdlemn4  40372  lcfrlem12N  40728  lcfrlem15  40731  lcdvscl  40779  lcdlssvscl  40780  lcdvsass  40781  lcdvs0N  40790  mapdincl  40835  mapdin  40836  mapdlsmcl  40837  mapdcnvatN  40840  mapdpglem2  40847  mapdpglem12  40857  mapdpglem18  40863  mapdpglem21  40866  mapdpglem22  40867  mapdpglem28  40875  mapdpglem30  40876  hdmaprnlem3N  41024  hdmaprnlem3uN  41025  hdmaprnlem7N  41029  hdmaprnlem8N  41030  hdmaprnlem9N  41031  hdmaprnlem3eN  41032  hdmaprnlem16N  41036  hgmapdcl  41064  hgmapval1  41067  hgmaprnlem4N  41073  hdmapinvlem1  41092  fzadd2d  41149  sticksstones1  41268  sticksstones8  41275  sticksstones9  41276  sticksstones10  41277  sticksstones11  41278  sticksstones17  41285  sticksstones18  41286  fnsnbt  41357  mhmcompl  41422  evlsbagval  41440  evlsevl  41445  evlvvval  41447  evlvvvallem  41448  selvcllem2  41452  evlselv  41461  mhpind  41468  fltnltalem  41706  wepwsolem  42086  kercvrlsm  42127  dfacbasgrp  42152  onexomgt  42292  onexoegt  42295  onov0suclim  42326  cantnftermord  42372  cantnf2  42377  omcl2  42385  ofoaf  42407  ofoafo  42408  imo72b2lem0  43219  grurankcld  43294  grumnudlem  43346  grumnud  43347  inaex  43358  gruex  43359  dvconstbi  43395  cncmpmax  44018  iooabslt  44510  fmul01lt1lem2  44599  limciccioolb  44635  limcicciooub  44651  limsuppnfdlem  44715  climrescn  44762  climxrrelem  44763  climxrre  44764  liminflimsupxrre  44831  xlimmnfvlem2  44847  xlimpnfvlem2  44851  fsumcncf  44892  ioccncflimc  44899  icocncflimc  44903  cncfiooicclem1  44907  dvbdfbdioolem2  44943  dvnmul  44957  stoweidlem26  45040  stoweidlem34  45048  stoweidlem48  45062  stoweidlem59  45073  dirkercncflem3  45119  fourierdlem32  45153  fourierdlem41  45162  fourierdlem51  45171  fourierdlem63  45183  fourierdlem82  45202  fourierdlem85  45205  fourierdlem93  45213  fourierdlem111  45231  fourierdlem114  45234  etransclem35  45283  hspdifhsp  45630  opnvonmbllem1  45646  ovnovollem1  45670  mbfresmf  45753  smfaddlem1  45777  smfsuplem1  45825  smflimsuplem5  45838  fzoopth  46333  setsidel  46342  setsnidel  46343  imasetpreimafvbijlemf  46367  prelspr  46452  rnghmsubcsetclem1  46961  rngccatidALTV  46975  zrinitorngc  46986  zrtermorngc  46987  zrzeroorngc  46988  rhmsubcsetclem1  47007  rhmsubcrngclem1  47013  funcringcsetcALTV2lem3  47024  funcringcsetcALTV2lem8  47029  ringccatidALTV  47038  funcringcsetclem3ALTV  47047  funcringcsetclem8ALTV  47052  irinitoringc  47055  zrtermoringc  47056  zrninitoringc  47057  nzerooringczr  47058  srhmsubclem2  47060  srhmsubc  47062  srhmsubcALTVlem1  47078  srhmsubcALTV  47080  rhmsubcALTVlem3  47092  lcosslsp  47206  nnolog2flm1  47363  glbprlem  47685  topdlat  47716  catprs  47718  mndtccatid  47800  grptcmon  47803  grptcepi  47804