Theorem eleqtrri 2862

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 2772	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2861	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  3eltr4i  2876  vex  3459  opi1  5450  opi2  5451  frrlem14  8292  seqomlem3  8435  nlim2  8471  oneo  8562  nnneo  8637  0elixp  8923  ac6sfi  9240  tz9.13  9759  rankval  9784  rankid  9801  ssrankr1  9803  rankel  9807  rankval3  9808  rankpw  9811  rankss  9817  ranksn  9822  rankuni2  9823  rankun  9824  rankpr  9825  rankop  9826  rankeq0  9829  rankr1b  9832  djuun  9908  dju1dif  10152  isfin4p1  10294  fin1a2lem4  10382  fin1a2lem6  10384  hsmexlem6  10410  dcomex  10426  axdc3lem4  10432  canthp1lem2  10633  pwxpndom2  10645  rankcf  10757  grutsk  10802  axgroth3  10811  inaprc  10816  1lt2pi  10885  pnfxr  11258  mnfxr  11261  1nn  12239  uzrdg0i  13991  axdc4uzlem  14015  ccat2s1p2  14664  wrdl3s3  14995  infcvgaux1i  15907  0bits  16492  sadcf  16506  prmreclem6  16976  fnpr2ob  17607  setcepi  18140  setc2obas  18146  setc2ohom  18147  cat1  18149  smndex1mnd  18967  smndex1id  18968  pwmnd  18994  grpss  19016  psgnunilem2  19560  psgnprfval2  19588  efgi0  19785  efgi1  19786  vrgpf  19833  vrgpinv  19834  frgpuptinv  19836  frgpup2  19841  frgpnabllem1  19938  dmdprdpr  20116  dprdpr  20117  pzriprnglem7  21637  pzriprnglem13  21643  pzriprng1ALT  21646  m2detleiblem3  22786  m2detleiblem4  22787  m2detleib  22788  leordtval2  23369  xpstopnlem1  23966  xpstopnlem2  23968  ptcmp  24215  tsmsfbas  24285  zcld  24971  sszcld  24975  abscncfALT  25083  iimulcn  25097  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  cnstrcvs  25300  cncvs  25304  dveflem  26138  ftc1  26201  efopnlem2  26822  cxpcn3  26913  efrlim  27134  precsexlem11  28410  1nns  28542  structvtxval  29371  usgrexmplef  29609  wwlks2onv  30302  elwwlks2ons3im  30303  usgrwwlks2on  30307  umgrwwlks2on  30308  konigsberglem4  30606  hhshsslem2  31620  nonbooli  32003  nmopadjlei  32440  cshw1s2  33280  fzto1st  33423  cyc2fv1  33441  cyc3fv1  33457  cyc3fv2  33458  cyc3evpm  33470  1arithidom  33827  zringpid  33842  vieta  33970  xrge0iifhmeo  34326  dya2iocbrsiga  34665  dya2icobrsiga  34666  fib0  34789  fib1  34790  coinflippvt  34875  prodfzo03  34990  circlevma  35029  circlemethhgt  35030  hgt750lemg  35041  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  tgoldbachgtde  35047  tgoldbachgt  35050  bnj97  35254  bnj553  35286  bnj966  35332  bnj1442  35437  fineqvnttrclse  35537  fineqvinfep  35538  subfacp1lem2a  35672  subfacp1lem5  35676  erdszelem5  35687  erdszelem8  35690  ex-sategoelel12  35919  rankeq1o  36663  0hf  36669  onint1  36980  regsfromunir1  37071  bj-0eltag  37634  bj-minftyccb  37889  finxpreclem4  38060  fdc  38416  reheibor  38510  0prjspnlem  43375  0prjspnrel  43379  pw2f1ocnv  43784  onexoegt  43991  2omomeqom  44050  omnord1ex  44051  oege2  44054  oenord1ex  44062  oenord1  44063  oaomoencom  44064  oenassex  44065  comptiunov2i  44452  clsk1indlem4  44790  clsk1indlem1  44791  mnuprdlem3  45004  sucidALTVD  45598  sucidALT  45599  sucidVD  45600  wfaxnul  45725  wfaxinf2  45730  nregmodellem  45745  rfcnpre1  45759  eliuniincex  45847  iocopn  46256  icoopn  46261  islptre  46355  cnrefiisplem  46563  icccncfext  46621  fourierdlem103  46943  fourierdlem104  46944  iooborel  47085  sprsymrelfo  48266  sbgoldbo  48572  stgr1  48746  isubgr3stgrlem7  48757  gpg3kgrtriexlem5  48872  pglem  48876  grlimedgnedg  48916  0even  49022  2even  49024  2zrngamgm  49030  zlmodzxzldeplem3  49302  rrx2pxel  49511  rrx2pyel  49512  rrx2linesl  49543  2sphere0  49550  i0oii  49718  io1ii  49719  setc1onsubc  50400