Theorem eleqtrri 2861

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837

This theorem is used by:  3eltr4i  2875  vex  3458  opi1  5449  opi2  5450  frrlem14  8294  seqomlem3  8437  nlim2  8473  oneo  8564  nnneo  8639  0elixp  8925  ac6sfi  9242  tz9.13  9761  rankval  9786  rankid  9803  ssrankr1  9805  rankel  9809  rankval3  9810  rankpw  9813  rankss  9819  ranksn  9824  rankuni2  9825  rankun  9826  rankpr  9827  rankop  9828  rankeq0  9831  rankr1b  9834  djuun  9919  dju1dif  10163  isfin4p1  10305  fin1a2lem4  10393  fin1a2lem6  10395  hsmexlem6  10421  dcomex  10437  axdc3lem4  10443  canthp1lem2  10644  pwxpndom2  10656  rankcf  10768  grutsk  10813  axgroth3  10822  inaprc  10827  1lt2pi  10896  pnfxr  11269  mnfxr  11272  1nn  12250  uzrdg0i  14002  axdc4uzlem  14026  ccat2s1p2  14675  wrdl3s3  15006  infcvgaux1i  15918  0bits  16503  sadcf  16517  prmreclem6  16987  fnpr2ob  17618  setcepi  18151  setc2obas  18157  setc2ohom  18158  cat1  18160  smndex1mnd  18978  smndex1id  18979  pwmnd  19005  grpss  19027  psgnunilem2  19571  psgnprfval2  19599  efgi0  19796  efgi1  19797  vrgpf  19844  vrgpinv  19845  frgpuptinv  19847  frgpup2  19852  frgpnabllem1  19949  dmdprdpr  20127  dprdpr  20128  pzriprnglem7  21648  pzriprnglem13  21654  pzriprng1ALT  21657  m2detleiblem3  22797  m2detleiblem4  22798  m2detleib  22799  leordtval2  23380  xpstopnlem1  23977  xpstopnlem2  23979  ptcmp  24226  tsmsfbas  24296  zcld  24982  sszcld  24986  abscncfALT  25094  iimulcn  25108  icopnfhmeo  25113  iccpnfhmeo  25115  xrhmeo  25116  cnstrcvs  25311  cncvs  25315  dveflem  26149  ftc1  26212  efopnlem2  26833  cxpcn3  26924  efrlim  27145  precsexlem11  28421  1nns  28553  structvtxval  29382  usgrexmplef  29620  wwlks2onv  30313  elwwlks2ons3im  30314  usgrwwlks2on  30318  umgrwwlks2on  30319  konigsberglem4  30617  hhshsslem2  31631  nonbooli  32014  nmopadjlei  32451  cshw1s2  33289  fzto1st  33432  cyc2fv1  33450  cyc3fv1  33466  cyc3fv2  33467  cyc3evpm  33479  1arithidom  33836  zringpid  33851  vieta  33979  xrge0iifhmeo  34335  dya2iocbrsiga  34674  dya2icobrsiga  34675  fib0  34798  fib1  34799  coinflippvt  34884  prodfzo03  34999  circlevma  35038  circlemethhgt  35039  hgt750lemg  35050  hgt750lemb  35052  hgt750lema  35053  hgt750leme  35054  tgoldbachgtde  35056  tgoldbachgt  35059  bnj97  35263  bnj553  35295  bnj966  35341  bnj1442  35446  fineqvnttrclse  35545  fineqvinfep  35546  subfacp1lem2a  35680  subfacp1lem5  35684  erdszelem5  35695  erdszelem8  35698  ex-sategoelel12  35927  rankeq1o  36671  0hf  36677  onint1  36988  regsfromunir1  37079  bj-0eltag  37642  bj-minftyccb  37897  finxpreclem4  38068  fdc  38424  reheibor  38518  0prjspnlem  43383  0prjspnrel  43387  pw2f1ocnv  43792  onexoegt  43999  2omomeqom  44058  omnord1ex  44059  oege2  44062  oenord1ex  44070  oenord1  44071  oaomoencom  44072  oenassex  44073  comptiunov2i  44460  clsk1indlem4  44798  clsk1indlem1  44799  mnuprdlem3  45012  sucidALTVD  45606  sucidALT  45607  sucidVD  45608  wfaxnul  45733  wfaxinf2  45738  nregmodellem  45753  rfcnpre1  45767  eliuniincex  45855  iocopn  46264  icoopn  46269  islptre  46363  cnrefiisplem  46571  icccncfext  46629  fourierdlem103  46951  fourierdlem104  46952  iooborel  47093  sprsymrelfo  48274  sbgoldbo  48580  stgr1  48754  isubgr3stgrlem7  48765  gpg3kgrtriexlem5  48880  pglem  48884  grlimedgnedg  48924  0even  49030  2even  49032  2zrngamgm  49038  zlmodzxzldeplem3  49310  rrx2pxel  49519  rrx2pyel  49520  rrx2linesl  49551  2sphere0  49558  i0oii  49726  io1ii  49727  setc1onsubc  50408