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 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  3eltr4i  2875  vex  3458  opi1  5436  opi2  5437  frrlem14  8280  seqomlem3  8423  nlim2  8459  oneo  8550  nnneo  8625  0elixp  8911  ac6sfi  9228  tz9.13  9749  rankval  9774  rankid  9791  ssrankr1  9793  rankel  9797  rankval3  9798  rankpw  9801  rankss  9807  ranksn  9812  rankuni2  9813  rankun  9814  rankpr  9815  rankop  9816  rankeq0  9819  rankr1b  9822  djuun  9884  dju1dif  10129  isfin4p1  10272  fin1a2lem4  10360  fin1a2lem6  10362  hsmexlem6  10388  dcomex  10404  axdc3lem4  10410  canthp1lem2  10611  pwxpndom2  10623  rankcf  10735  grutsk  10780  axgroth3  10789  inaprc  10794  1lt2pi  10863  pnfxr  11236  mnfxr  11239  1nn  12221  uzrdg0i  13972  axdc4uzlem  13996  ccat2s1p2  14644  wrdl3s3  14975  infcvgaux1i  15887  0bits  16473  sadcf  16487  prmreclem6  16957  fnpr2ob  17588  setcepi  18121  setc2obas  18127  setc2ohom  18128  cat1  18130  smndex1mnd  18947  smndex1id  18948  pwmnd  18974  grpss  18996  psgnunilem2  19535  psgnprfval2  19563  efgi0  19760  efgi1  19761  vrgpf  19808  vrgpinv  19809  frgpuptinv  19811  frgpup2  19816  frgpnabllem1  19913  dmdprdpr  20091  dprdpr  20092  pzriprnglem7  21539  pzriprnglem13  21545  pzriprng1ALT  21548  m2detleiblem3  22689  m2detleiblem4  22690  m2detleib  22691  leordtval2  23272  xpstopnlem1  23869  xpstopnlem2  23871  ptcmp  24118  tsmsfbas  24188  zcld  24874  sszcld  24878  abscncfALT  24986  iimulcn  25000  icopnfhmeo  25005  iccpnfhmeo  25007  xrhmeo  25008  cnstrcvs  25203  cncvs  25207  dveflem  26041  ftc1  26104  efopnlem2  26722  cxpcn3  26813  efrlim  27034  precsexlem11  28310  1nns  28442  structvtxval  29222  usgrexmplef  29460  wwlks2onv  30153  elwwlks2ons3im  30154  usgrwwlks2on  30158  umgrwwlks2on  30159  konigsberglem4  30457  hhshsslem2  31471  nonbooli  31854  nmopadjlei  32291  cshw1s2  33138  fzto1st  33283  cyc2fv1  33301  cyc3fv1  33317  cyc3fv2  33318  cyc3evpm  33330  1arithidom  33733  zringpid  33748  vieta  33877  xrge0iifhmeo  34233  dya2iocbrsiga  34572  dya2icobrsiga  34573  fib0  34696  fib1  34697  coinflippvt  34782  prodfzo03  34897  circlevma  34936  circlemethhgt  34937  hgt750lemg  34948  hgt750lemb  34950  hgt750lema  34951  hgt750leme  34952  tgoldbachgtde  34954  tgoldbachgt  34957  bnj97  35161  bnj553  35193  bnj966  35239  bnj1442  35344  fineqvnttrclse  35420  fineqvinfep  35421  subfacp1lem2a  35530  subfacp1lem5  35534  erdszelem5  35545  erdszelem8  35548  ex-sategoelel12  35777  rankeq1o  36521  0hf  36527  onint1  36809  regsfromunir1  36900  bj-0eltag  37463  bj-minftyccb  37717  finxpreclem4  37888  fdc  38244  reheibor  38338  0prjspnlem  43205  0prjspnrel  43209  pw2f1ocnv  43614  onexoegt  43821  2omomeqom  43880  omnord1ex  43881  oege2  43884  oenord1ex  43892  oenord1  43893  oaomoencom  43894  oenassex  43895  comptiunov2i  44282  clsk1indlem4  44620  clsk1indlem1  44621  mnuprdlem3  44850  sucidALTVD  45445  sucidALT  45446  sucidVD  45447  wfaxnul  45572  wfaxinf2  45577  nregmodellem  45592  rfcnpre1  45599  eliuniincex  45687  iocopn  46096  icoopn  46101  islptre  46195  cnrefiisplem  46403  icccncfext  46461  fourierdlem103  46783  fourierdlem104  46784  iooborel  46925  sprsymrelfo  48103  sbgoldbo  48409  stgr1  48583  isubgr3stgrlem7  48594  gpg3kgrtriexlem5  48709  pglem  48713  grlimedgnedg  48753  0even  48859  2even  48861  2zrngamgm  48867  zlmodzxzldeplem3  49124  rrx2pxel  49333  rrx2pyel  49334  rrx2linesl  49365  2sphere0  49372  i0oii  49541  io1ii  49542  setc1onsubc  50223