Theorem eleqtrri 2868

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtrri.1	⊢ 𝐴 ∈ 𝐵
eleqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrri.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2778	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2867	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  3eltr4i  2882  vex  3467  opi1  5451  opi2  5452  frrlem14  8296  seqomlem3  8439  nlim2  8475  oneo  8566  nnneo  8641  0elixp  8927  ac6sfi  9244  tz9.13  9763  rankval  9788  rankid  9805  ssrankr1  9807  rankel  9811  rankval3  9812  rankpw  9815  rankss  9821  ranksn  9826  rankuni2  9827  rankun  9828  rankpr  9829  rankop  9830  rankeq0  9833  rankr1b  9836  djuun  9912  dju1dif  10156  isfin4p1  10299  fin1a2lem4  10387  fin1a2lem6  10389  hsmexlem6  10415  dcomex  10431  axdc3lem4  10437  canthp1lem2  10638  pwxpndom2  10650  rankcf  10762  grutsk  10807  axgroth3  10816  inaprc  10821  1lt2pi  10890  pnfxr  11263  mnfxr  11266  1nn  12244  uzrdg0i  13995  axdc4uzlem  14019  ccat2s1p2  14668  wrdl3s3  14999  infcvgaux1i  15911  0bits  16497  sadcf  16511  prmreclem6  16981  fnpr2ob  17612  setcepi  18145  setc2obas  18151  setc2ohom  18152  cat1  18154  smndex1mnd  18972  smndex1id  18973  pwmnd  18999  grpss  19021  psgnunilem2  19565  psgnprfval2  19593  efgi0  19790  efgi1  19791  vrgpf  19838  vrgpinv  19839  frgpuptinv  19841  frgpup2  19846  frgpnabllem1  19943  dmdprdpr  20121  dprdpr  20122  pzriprnglem7  21606  pzriprnglem13  21612  pzriprng1ALT  21615  m2detleiblem3  22755  m2detleiblem4  22756  m2detleib  22757  leordtval2  23338  xpstopnlem1  23935  xpstopnlem2  23937  ptcmp  24184  tsmsfbas  24254  zcld  24940  sszcld  24944  abscncfALT  25052  iimulcn  25066  icopnfhmeo  25071  iccpnfhmeo  25073  xrhmeo  25074  cnstrcvs  25269  cncvs  25273  dveflem  26107  ftc1  26170  efopnlem2  26788  cxpcn3  26879  efrlim  27100  precsexlem11  28376  1nns  28508  structvtxval  29312  usgrexmplef  29550  wwlks2onv  30243  elwwlks2ons3im  30244  usgrwwlks2on  30248  umgrwwlks2on  30249  konigsberglem4  30547  hhshsslem2  31561  nonbooli  31944  nmopadjlei  32381  cshw1s2  33221  fzto1st  33364  cyc2fv1  33382  cyc3fv1  33398  cyc3fv2  33399  cyc3evpm  33411  1arithidom  33772  zringpid  33787  vieta  33915  xrge0iifhmeo  34271  dya2iocbrsiga  34610  dya2icobrsiga  34611  fib0  34734  fib1  34735  coinflippvt  34820  prodfzo03  34935  circlevma  34974  circlemethhgt  34975  hgt750lemg  34986  hgt750lemb  34988  hgt750lema  34989  hgt750leme  34990  tgoldbachgtde  34992  tgoldbachgt  34995  bnj97  35199  bnj553  35231  bnj966  35277  bnj1442  35382  fineqvnttrclse  35460  fineqvinfep  35461  subfacp1lem2a  35571  subfacp1lem5  35575  erdszelem5  35586  erdszelem8  35589  ex-sategoelel12  35818  rankeq1o  36562  0hf  36568  onint1  36849  regsfromunir1  36940  bj-0eltag  37502  bj-minftyccb  37757  finxpreclem4  37928  fdc  38284  reheibor  38378  0prjspnlem  43247  0prjspnrel  43251  pw2f1ocnv  43656  onexoegt  43863  2omomeqom  43922  omnord1ex  43923  oege2  43926  oenord1ex  43934  oenord1  43935  oaomoencom  43936  oenassex  43937  comptiunov2i  44324  clsk1indlem4  44662  clsk1indlem1  44663  mnuprdlem3  44876  sucidALTVD  45470  sucidALT  45471  sucidVD  45472  wfaxnul  45597  wfaxinf2  45602  nregmodellem  45617  rfcnpre1  45631  eliuniincex  45719  iocopn  46128  icoopn  46133  islptre  46227  cnrefiisplem  46435  icccncfext  46493  fourierdlem103  46815  fourierdlem104  46816  iooborel  46957  sprsymrelfo  48135  sbgoldbo  48441  stgr1  48615  isubgr3stgrlem7  48626  gpg3kgrtriexlem5  48741  pglem  48745  grlimedgnedg  48785  0even  48891  2even  48893  2zrngamgm  48899  zlmodzxzldeplem3  49167  rrx2pxel  49376  rrx2pyel  49377  rrx2linesl  49408  2sphere0  49415  i0oii  49583  io1ii  49584  setc1onsubc  50265