Theorem eleqtrrd 2831

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  3eltr4d  2843  rspc2vd  3907  disjxiun  5099  eldmressnsn  5984  fnsnbg  7120  elimdelov  7465  elovmpt3rab1  7629  fnwelem  8087  tfrlem13  8335  tz7.44-2  8352  omordi  8507  oneo  8522  omeulem2  8524  oeordi  8528  oeeui  8543  nnneo  8596  naddelim  8627  erref  8668  en1uniel  8977  omxpenlem  9019  unblem3  9217  dffi3  9358  ordtypelem10  9456  oismo  9469  cantnff  9603  cantnfp1lem3  9609  cantnflem1  9618  cnfcom  9629  r1ordg  9707  r1pwss  9713  rankwflemb  9722  r1elwf  9725  rankidb  9729  rankonidlem  9757  fseqenlem2  9954  dfac12lem1  10073  dfac12lem2  10074  pwsdompw  10132  ackbij2lem3  10169  ackbij2  10171  cfsmolem  10199  hsmexlem4  10358  ttukeylem3  10440  ttukeylem7  10444  iundom2g  10469  fpwwe2lem8  10567  canthwelem  10579  pwfseqlem4  10591  winalim2  10625  r1wunlim  10666  tskmid  10769  fzopth  13498  predfz  13590  fzoss2  13624  fz1fzo0m1  13647  fzo0addel  13655  fzo0addelr  13656  elfzoext  13659  fzosubel3  13663  elfzomin  13674  elfzonlteqm1  13678  fzoend  13694  fzoopth  13699  fzofzp1  13701  fzofzp1b  13702  peano2fzor  13711  zmodfzo  13832  seqf1olem2  13983  bcn2  14260  swrdccat2  14610  pfxccat1  14643  swrdswrd  14646  pfxccatin12  14674  splfv1  14696  revcl  14702  revlen  14703  revccat  14707  revrev  14708  repswpfx  14726  cshwidxmod  14744  revco  14776  limsupgre  15423  summolem2a  15657  fsumm1  15693  fsumcom2  15716  prodmolem2a  15876  fprodm1  15909  fprodcom2  15926  prmreclem4  16866  prmreclem5  16867  vdwapid1  16922  vdwlem5  16932  vdwlem8  16935  vdwnnlem2  16943  ramub1lem1  16973  ramub1lem2  16974  mrieqvlemd  17570  mreexd  17583  mreexexlemd  17585  catcocl  17626  catass  17627  moni  17678  epii  17685  inviso1  17708  episect  17727  invisoinvl  17732  catsubcat  17781  subccocl  17787  fullsubc  17792  funcco  17813  resf2nd  17837  funcres  17838  fthepi  17872  nati  17900  arwhoma  17987  catccatid  18048  resscatc  18051  catcisolem  18052  catcoppccl  18059  catcfuccl  18060  estrreslem2  18079  funcestrcsetclem3  18083  funcestrcsetclem8  18088  equivestrcsetc  18093  funcsetcestrclem3  18097  funcsetcestrclem8  18103  xpcco  18124  xpcco2  18128  xpccatid  18129  prfcl  18144  catcxpccl  18148  curf12  18168  curf1cl  18169  curf2  18170  curf2cl  18172  curfcl  18173  uncf2  18178  uncfcurf  18180  diag12  18185  diag2  18186  curf2ndf  18188  hofcl  18200  oppchofcl  18201  oyoncl  18211  yonedalem3a  18215  yonedalem4b  18217  yonedalem22  18219  yonedalem3b  18220  yonedalem3  18221  yonedainv  18222  yonffthlem  18223  latcl2  18377  latlem  18378  latjcom  18388  latmcom  18404  clatlem  18443  clatlubcl2  18445  clatglbcl2  18447  acsfiindd  18494  gsumpropd2lem  18588  sgrppropd  18640  mndpropd  18668  imasmnd  18684  frmdmnd  18768  frmdgsum  18771  grpsubpropd2  18960  imasgrp  18970  subg0  19046  0ghm  19144  resghm2  19147  ghmco  19150  pwsdiagghm  19158  ghmqusnsglem2  19195  ghmqusnsg  19196  ghmquskerlem2  19199  ghmquskerlem3  19200  ghmqusker  19201  psgnunilem1  19407  psgnunilem5  19408  psgnunilem2  19409  psgnunilem3  19410  sylow1lem4  19515  sylow1lem5  19516  efglem  19630  efgtf  19636  efginvrel2  19641  efginvrel1  19642  efgsdmi  19646  efgs1b  19650  efgsres  19652  efgsfo  19653  efgredleme  19657  efgredlemc  19659  efgredlem  19661  efgcpbllemb  19669  frgp0  19674  frgpadd  19677  frgpinv  19678  vrgpf  19682  vrgpinv  19683  frgpuplem  19686  frgpup1  19689  frgpup2  19690  frgpup3lem  19691  frgpnabllem1  19787  frgpnabllem2  19788  gsumval3  19821  dprdfid  19933  dprdsn  19952  dprd2da  19958  dpjidcl  19974  pgpfac1lem2  19991  pgpfaclem3  19999  ablsimpg1gend  20021  ablsimpgprmd  20031  rngpropd  20094  imasrng  20097  ringpropd  20208  imasring  20250  qusring2  20254  pwsco1rhm  20422  pwsco2rhm  20423  lringuplu  20464  subrgunit  20510  pwsdiagrhm  20527  rnghmsubcsetclem1  20551  zrinitorngc  20562  zrtermorngc  20563  zrzeroorngc  20564  rhmsubcsetclem1  20580  rhmsubcrngclem1  20586  zrtermoringc  20595  zrninitoringc  20596  srhmsubclem2  20598  srhmsubc  20600  cntzsdrg  20722  isabvd  20732  lmodprop2d  20862  islssd  20873  prdsvscacl  20906  prdslmodd  20907  islmhm2  20977  lmhmco  20982  lmhmplusg  20983  lmhmvsca  20984  lmhmpropd  21012  lsppreli  21029  ellspsn4  21066  lssacsex  21086  lspsnat  21087  lidlnsg  21190  qus2idrng  21215  qus1  21216  qusrhm  21218  rhmpreimaidl  21219  rhmqusnsg  21227  rngqiprngghmlem1  21229  rngqiprngfulem1  21253  irinitoringc  21421  nzerooringczr  21422  znf1o  21493  cssmre  21635  dsmmlss  21686  frlmsplit2  21715  frlmbas3  21718  frlmup1  21740  assapropd  21814  psr0cl  21894  psrnegcl  21896  psr1cl  21903  resspsrmul  21918  subrgpsr  21920  mvrf  21927  mplmon  21975  mplcoe1  21977  subrgasclcl  22007  mplind  22010  evlslem1  22022  subrgply1  22150  psrplusgpropd  22153  ply1coe  22218  cply1coe0bi  22222  lply1binomsc  22231  ply1fermltlchr  22232  evls1val  22240  evls1rhm  22242  evl1val  22249  evl1rhm  22252  pf1ind  22275  evl1scvarpw  22283  evls1fpws  22289  mhmcompl  22300  rhmply1  22306  matbas2i  22342  matplusg2  22347  matvsca2  22348  matsubgcell  22354  matvscacell  22356  mpomatmul  22366  mavmulval  22465  mavmulcl  22467  mavmulass  22469  mavmul0  22472  mavmumamul1  22475  m1detdiag  22517  cramerimplem2  22604  mat2pmatmul  22651  mat2pmatlin  22655  monmatcollpw  22699  pmatcollpwfi  22702  mply1topmatcl  22725  pm2mpghm  22736  pm2mpmhmlem2  22739  pm2mp  22745  chpmat1dlem  22755  chpmat1d  22756  chpdmatlem0  22757  chpscmat  22762  chpscmatgsumbin  22764  chpscmatgsummon  22765  chfacfscmulcl  22777  cpmadugsumlemB  22794  cpmadugsumlemC  22795  chcoeffeqlem  22805  cldmreon  23014  neiptopreu  23053  maxlp  23067  ordttopon  23113  ordtrest2lem  23123  cnprcl2  23171  lmcnp  23224  resthauslem  23283  hauscmplem  23326  1stcfb  23365  2ndcctbss  23375  2ndcomap  23378  dis2ndc  23380  loclly  23407  hausllycmp  23414  locfincmp  23446  dissnref  23448  kgeni  23457  kgenidm  23467  ptpjpre2  23500  xkoopn  23509  txopn  23522  ptpjopn  23532  ptcldmpt  23534  ptcls  23536  pthaus  23558  txkgen  23572  xkohaus  23573  xkopt  23575  txconn  23609  imastps  23641  kqid  23648  kqopn  23654  kqcld  23655  isr0  23657  indishmph  23718  pt1hmeo  23726  ptuncnv  23727  ptunhmeo  23728  t0kq  23738  filconn  23803  uzrest  23817  uffixsn  23845  fmfnfmlem2  23875  flimss2  23892  flimss1  23893  flimclslem  23904  flfcnp  23924  fclsfnflim  23947  uffclsflim  23951  fcfelbas  23956  alexsublem  23964  alexsub  23965  cnextcn  23987  cnextfres1  23988  cnextfres  23989  tmdgsum  24015  distgp  24019  indistgp  24020  symgtgp  24026  ghmcnp  24035  qustgpopn  24040  qustgplem  24041  qustgphaus  24043  prdstmdd  24044  prdstgpd  24045  tsmsid  24060  tsmssubm  24063  tsmsmhm  24066  tsmsadd  24067  tsmssplit  24072  utop2nei  24171  utop3cls  24172  neipcfilu  24216  cnextucn  24223  ucnextcn  24224  blpnfctr  24357  lpbl  24424  met2ndci  24443  tmsxps  24457  metcnpi  24465  metcnpi2  24466  metcnpi3  24467  metustid  24475  metustsym  24476  metustexhalf  24477  subgngp  24556  ngptgp  24557  sranlm  24605  nlmvscn  24608  nrginvrcn  24613  lssnlm  24622  nghmcn  24666  iccntr  24743  icccmplem2  24745  msdcn  24763  cncfmptc  24838  cncfmptid  24839  cncfmpt2f  24841  icoopnst  24869  iocopnst  24870  nmoleub2lem3  25048  nmoleub3  25052  nmhmcn  25053  ipcn  25179  cfilfcls  25207  caucfil  25216  equivcau  25233  caubl  25241  flimcfil  25247  cmssmscld  25283  rrxdstprj1  25342  minveclem3b  25361  minveclem4  25365  mulcncf  25379  ovolicc2lem3  25453  ovolicc2lem4  25454  opnmbllem  25535  vitalilem2  25543  mbfsup  25598  mbfinf  25599  mbfi1fseqlem4  25652  limccnp  25825  limccnp2  25826  dvreslem  25843  dvres2lem  25844  dvidlem  25849  dvcnp2  25854  dvcnp2OLD  25855  dvcn  25856  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcmul  25880  dvcof  25885  dvcnvlem  25913  dvef  25917  rollelem  25926  dvlip2  25933  dvivthlem1  25946  dvivth  25948  lhop2  25953  lhop  25954  dvcnvrelem1  25955  dvcnvrelem2  25956  dvcnvre  25957  ply1rem  26104  fta1blem  26109  plycpn  26230  plyrem  26246  tayl0  26302  dvtaylp  26311  dvntaylp  26312  dvntaylp0  26313  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem3  26344  psercn  26369  pserdv  26372  abelth  26384  efabl  26492  efopnlem1  26598  loglesqrt  26704  relogbf  26734  efrlim  26912  efrlimOLD  26913  dchrghm  27200  dchrptlem3  27210  nodenselem5  27633  nosupres  27652  noinfres  27667  sltlpss  27857  precsexlem11  28159  noseq0  28224  noseqp1  28225  noseqrdgfn  28240  noseqrdgsuc  28242  tgbtwntriv2  28467  tgbtwnne  28470  ercgrg  28497  tgidinside  28551  tgbtwnconn1  28555  tglnne  28608  tglnne0  28620  tglnpt2  28621  tglineneq  28624  ncolncol  28626  coltr3  28628  mirln  28656  mirln2  28657  mirconn  28658  krippenlem  28670  footexALT  28698  footexlem1  28699  footexlem2  28700  colperpexlem3  28712  mideulem2  28714  opphllem  28715  oppne3  28723  opphllem1  28727  opphllem2  28728  opphllem4  28730  oppperpex  28733  opphl  28734  hlpasch  28736  hpgerlem  28745  colhp  28750  midbtwn  28759  lmieu  28764  lmiisolem  28776  sacgr  28811  f1otrg  28851  f1otrge  28852  ebtwntg  28962  ecgrtg  28963  eengtrkg  28966  eengtrkge  28967  upgr1eop  29095  usgredg3  29196  uspgr1eop  29227  usgr1eop  29230  vtxdun  29462  vtxdfiun  29463  1loopgruspgr  29481  1loopgrvd2  29484  1hevtxdg1  29487  1egrvtxdg1  29490  1egrvtxdg0  29492  umgr2v2e  29506  wlkres  29649  wlkp1lem4  29655  wlkp1  29660  cyclnumvtx  29780  wwlksm1edg  29861  wwlksnext  29873  wwlksnextproplem3  29891  clwwlkel  30025  1wlkdlem2  30117  trlsegvdeg  30206  eupth2lem3lem1  30207  eupth2lem3lem2  30208  extwwlkfab  30331  numclwlk2lem2f  30356  spansnid  31542  elspansn4  31552  fnpreimac  32645  ccatf1  32920  ccatws1f1olast  32924  swrdrn2  32926  swrdrn3  32927  swrdf1  32928  splfv3  32930  pwrssmgc  32972  pfxchn  32981  chnind  32983  chnub  32984  chnlt  32985  wrdpmtrlast  33065  psgnfzto1stlem  33072  cycpmfv1  33085  cycpmfv2  33086  cycpmco2lem2  33099  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2  33105  cyc3co2  33112  cycpmrn  33115  submarchi  33155  subrdom  33251  fracfld  33274  imaslmod  33317  quslmod  33322  quslmhm  33323  nsgqusf1olem2  33378  lmhmqusker  33381  rhmquskerlem  33389  idlinsubrg  33395  drngidl  33397  rhmpreimaprmidl  33415  qsidomlem2  33417  mxidlprm  33434  opprmxidlabs  33451  qsdrngilem  33458  qsdrngi  33459  qsdrnglem2  33460  idlsrg0g  33470  pidufd  33507  dfufd2lem  33513  fply1  33520  evl1fpws  33526  ressply1evls1  33527  ressply1sub  33532  ply1asclunit  33536  r1plmhm  33568  drgextlsp  33582  matdim  33604  ply1degltdimlem  33611  lindsunlem  33613  qusdimsum  33617  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  extdg1id  33654  evls1fldgencl  33658  irngss  33675  irngnzply1  33679  minplymindeg  33691  minplyirredlem  33693  irredminply  33699  algextdeglem2  33701  constrconj  33728  constrfiss  33734  1smat1  33787  submat1n  33788  lmatfval  33797  lmatcl  33799  mdetpmtr1  33806  madjusmdetlem4  33813  qtopt1  33818  qtophaus  33819  locfinref  33824  zarcls1  33852  zarclsiin  33854  zarmxt1  33863  zarcmplem  33864  rhmpreimacn  33868  ordtrest2NEWlem  33905  elzrhunit  33960  qqhcn  33974  qqhucn  33975  esumel  34030  esumsplit  34036  sigagenss2  34133  elsx  34177  sxbrsigalem0  34255  dya2icoseg  34261  eulerpartlemb  34352  eulerpartlemgvv  34360  iwrdsplit  34371  sseqfv2  34378  probfinmeasb  34412  dstrvprob  34456  dstfrvel  34458  ballotlemrv  34504  signstfvn  34553  signstfvp  34555  signstfveq0  34561  signsvtp  34567  signsvtn  34568  reprsuc  34599  reprpmtf1o  34610  lpadleft  34667  bnj1006  34943  bnj1018g  34946  bnj1018  34947  bnj1121  34968  bnj1398  35017  bnj1450  35033  bnj1501  35050  revpfxsfxrev  35096  swrdrevpfx  35097  pfxwlk  35104  revwlk  35105  swrdwlk  35107  subfacp1lem5  35164  ptpconn  35213  indispconn  35214  cvxsconn  35223  cvmseu  35256  cvmliftmolem2  35262  cvmliftlem7  35271  cvmliftlem10  35274  cvmliftlem13  35276  cvmlift2lem12  35294  satfv1lem  35342  satffunlem1lem2  35383  satffunlem2lem2  35386  satefvfmla1  35405  mrsubcv  35490  mrsubff  35492  mrsubrn  35493  mrsubccat  35498  elmrsubrn  35500  mrsubco  35501  mrsubvrs  35502  mvhf  35538  msubvrs  35540  mclsax  35549  r1peuqusdeg1  35623  linerflx1  36130  linerflx2  36132  fwddifnval  36144  elhf2  36156  neibastop2lem  36341  weiunpo  36446  weiunso  36447  icoreunrn  37340  relowlssretop  37344  sucneqond  37346  matunitlindflem2  37604  poimirlem4  37611  poimirlem20  37627  poimirlem30  37637  broucube  37641  opnmbllem0  37643  areacirclem2  37696  areacirclem4  37698  blssp  37743  sstotbnd2  37761  totbndbnd  37776  prdstotbnd  37781  cnpwstotbnd  37784  heiborlem9  37806  exidcl  37863  exidresid  37866  grpokerinj  37880  iscringd  37985  erimeq2  38663  prter3  38868  toycom  38959  islfld  39048  lshpsmreu  39095  ldualelvbase  39113  ldualssvscl  39144  lkreqN  39156  lkrlspeqN  39157  erng1lem  40974  erngdvlem4  40978  erng0g  40981  erng1r  40982  erngdvlem4-rN  40986  dva0g  41014  dia1dim2  41049  dia1dimid  41050  dia2dimlem5  41055  dvhelvbasei  41075  dvhvaddass  41084  tendoinvcl  41091  tendolinv  41092  tendorinv  41093  dvhgrp  41094  dvhlveclem  41095  cdlemn4  41185  lcfrlem12N  41541  lcfrlem15  41544  lcdvscl  41592  lcdlssvscl  41593  lcdvsass  41594  lcdvs0N  41603  mapdincl  41648  mapdin  41649  mapdlsmcl  41650  mapdcnvatN  41653  mapdpglem2  41660  mapdpglem12  41670  mapdpglem18  41676  mapdpglem21  41679  mapdpglem22  41680  mapdpglem28  41688  mapdpglem30  41689  hdmaprnlem3N  41837  hdmaprnlem3uN  41838  hdmaprnlem7N  41842  hdmaprnlem8N  41843  hdmaprnlem9N  41844  hdmaprnlem3eN  41845  hdmaprnlem16N  41849  hgmapdcl  41877  hgmapval1  41880  hgmaprnlem4N  41886  hdmapinvlem1  41905  fzadd2d  41959  aks6d1c2lem4  42108  sticksstones1  42127  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones17  42144  sticksstones18  42145  aks6d1c6lem4  42154  rhmqusspan  42166  aks5lem2  42168  mhmcopsr  42530  evlsbagval  42547  evlsevl  42552  evlvvval  42554  evlvvvallem  42555  selvcllem2  42559  evlselv  42568  mhpind  42575  fltnltalem  42643  wepwsolem  43024  kercvrlsm  43065  dfacbasgrp  43090  onexomgt  43223  onexoegt  43226  onov0suclim  43256  cantnftermord  43302  cantnf2  43307  omcl2  43315  ofoaf  43337  ofoafo  43338  grurankcld  44215  grumnudlem  44267  grumnud  44268  inaex  44279  gruex  44280  dvconstbi  44316  cncmpmax  45019  iooabslt  45490  fmul01lt1lem2  45576  limciccioolb  45612  limcicciooub  45628  limsuppnfdlem  45692  climrescn  45739  climxrrelem  45740  climxrre  45741  liminflimsupxrre  45808  xlimmnfvlem2  45824  xlimpnfvlem2  45828  fsumcncf  45869  ioccncflimc  45876  icocncflimc  45880  cncfiooicclem1  45884  dvbdfbdioolem2  45920  dvnmul  45934  dvnprodlem1  45937  stoweidlem26  46017  stoweidlem34  46025  stoweidlem48  46039  stoweidlem59  46050  dirkercncflem3  46096  fourierdlem32  46130  fourierdlem41  46139  fourierdlem51  46148  fourierdlem63  46160  fourierdlem82  46179  fourierdlem85  46182  fourierdlem93  46190  fourierdlem111  46208  fourierdlem114  46211  etransclem35  46260  hspdifhsp  46607  opnvonmbllem1  46623  ovnovollem1  46647  mbfresmf  46730  smfaddlem1  46754  smfsuplem1  46802  smflimsuplem5  46815  setsidel  47370  setsnidel  47371  imasetpreimafvbijlemf  47395  prelspr  47480  upgrimpths  47902  gpgprismgr4cycllem9  48086  rngccatidALTV  48253  rhmsubcALTVlem3  48264  funcringcsetcALTV2lem3  48273  funcringcsetcALTV2lem8  48278  ringccatidALTV  48287  funcringcsetclem3ALTV  48296  funcringcsetclem8ALTV  48301  srhmsubcALTVlem1  48304  srhmsubcALTV  48306  lcosslsp  48420  nnolog2flm1  48572  ffvbr  48837  glbprlem  48946  topdlat  48985  catprs  48993  iinfsubc  49040  iinfconstbaslem  49047  imaid  49136  fthcomf  49139  uptr2  49203  natoppf2  49212  natoppfb  49213  swapf2  49256  swapfiso  49267  swapciso  49268  oppc1stflem  49269  cofuswapf2  49277  fuco22natlem  49327  fucoppcffth  49393  oppcthinco  49421  oppcthinendcALT  49423  thinccisod  49436  termco  49463  termchommo  49467  termcid  49468  termcterm  49495  termcterm2  49496  diagciso  49521  diagcic  49522  funcsn  49523  uobeqterm  49528  mndtccatid  49569  grptcmon  49575  grptcepi  49576  2arwcat  49582  lanval2  49609  ranval2  49612  lanup  49623  ranup  49624  lmddu  49649