Theorem eleqtrri 2836

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr4i  2850  vex  3446  opi1  5424  opi2  5425  frrlem14  8251  seqomlem3  8393  nlim2  8427  oneo  8518  nnneo  8593  0elixp  8879  ac6sfi  9196  tz9.13  9715  rankval  9740  rankid  9757  ssrankr1  9759  rankel  9763  rankval3  9764  rankpw  9767  rankss  9773  ranksn  9778  rankuni2  9779  rankun  9780  rankpr  9781  rankop  9782  rankeq0  9785  rankr1b  9788  djuun  9850  dju1dif  10095  isfin4p1  10237  fin1a2lem4  10325  fin1a2lem6  10327  hsmexlem6  10353  dcomex  10369  axdc3lem4  10375  canthp1lem2  10576  pwxpndom2  10588  rankcf  10700  grutsk  10745  axgroth3  10754  inaprc  10759  1lt2pi  10828  pnfxr  11198  mnfxr  11201  1nn  12168  uzrdg0i  13894  axdc4uzlem  13918  ccat2s1p2  14566  wrdl3s3  14897  infcvgaux1i  15792  0bits  16378  sadcf  16392  prmreclem6  16861  fnpr2ob  17491  setcepi  18024  setc2obas  18030  setc2ohom  18031  cat1  18033  smndex1mnd  18847  smndex1id  18848  pwmnd  18874  grpss  18896  psgnunilem2  19436  psgnprfval2  19464  efgi0  19661  efgi1  19662  vrgpf  19709  vrgpinv  19710  frgpuptinv  19712  frgpup2  19717  frgpnabllem1  19814  dmdprdpr  19992  dprdpr  19993  pzriprnglem7  21454  pzriprnglem13  21460  pzriprng1ALT  21463  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  leordtval2  23168  xpstopnlem1  23765  xpstopnlem2  23767  ptcmp  24014  tsmsfbas  24084  zcld  24770  sszcld  24774  abscncfALT  24886  iimulcn  24902  iimulcnOLD  24903  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  cnstrcvs  25109  cncvs  25113  dveflem  25951  ftc1  26017  efopnlem2  26634  cxpcn3  26726  efrlim  26947  efrlimOLD  26948  precsexlem11  28225  1nns  28357  structvtxval  29106  usgrexmplef  29344  wwlks2onv  30038  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  konigsberglem4  30342  hhshsslem2  31356  nonbooli  31739  nmopadjlei  32176  cshw1s2  33053  fzto1st  33197  cyc2fv1  33215  cyc3fv1  33231  cyc3fv2  33232  cyc3evpm  33244  1arithidom  33630  zringpid  33645  vieta  33757  xrge0iifhmeo  34114  dya2iocbrsiga  34453  dya2icobrsiga  34454  fib0  34577  fib1  34578  coinflippvt  34663  prodfzo03  34781  circlevma  34820  circlemethhgt  34821  hgt750lemg  34832  hgt750lemb  34834  hgt750lema  34835  hgt750leme  34836  tgoldbachgtde  34838  tgoldbachgt  34841  bnj97  35042  bnj553  35074  bnj966  35120  bnj1442  35225  fineqvnttrclse  35302  fineqvinfep  35303  subfacp1lem2a  35396  subfacp1lem5  35400  erdszelem5  35411  erdszelem8  35414  ex-sategoelel12  35643  rankeq1o  36387  0hf  36393  onint1  36665  regsfromunir1  36692  bj-0eltag  37226  bj-minftyccb  37480  finxpreclem4  37649  fdc  37996  reheibor  38090  0prjspnlem  42981  0prjspnrel  42985  pw2f1ocnv  43394  onexoegt  43601  2omomeqom  43660  omnord1ex  43661  oege2  43664  oenord1ex  43672  oenord1  43673  oaomoencom  43674  oenassex  43675  comptiunov2i  44062  clsk1indlem4  44400  clsk1indlem1  44401  mnuprdlem3  44630  sucidALTVD  45225  sucidALT  45226  sucidVD  45227  wfaxnul  45352  wfaxinf2  45357  nregmodellem  45372  rfcnpre1  45379  eliuniincex  45468  iocopn  45880  icoopn  45885  islptre  45979  cnrefiisplem  46187  icccncfext  46245  fourierdlem103  46567  fourierdlem104  46568  iooborel  46709  sprsymrelfo  47857  sbgoldbo  48147  stgr1  48321  isubgr3stgrlem7  48332  gpg3kgrtriexlem5  48447  pglem  48451  grlimedgnedg  48491  0even  48597  2even  48599  2zrngamgm  48605  zlmodzxzldeplem3  48862  rrx2pxel  49071  rrx2pyel  49072  rrx2linesl  49103  2sphere0  49110  i0oii  49279  io1ii  49280  setc1onsubc  49961