Theorem eleqtrri 2838

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

Syntax hints:   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  3eltr4i  2852  vex  3426  vexOLD  3427  opi1  5377  opi2  5378  frrlem14  8086  wfrlem14OLD  8124  wfrlem16OLD  8126  seqomlem3  8253  oneo  8374  nnneo  8445  0elixp  8675  ac6sfi  8988  tz9.13  9480  rankval  9505  rankid  9522  ssrankr1  9524  rankel  9528  rankval3  9529  rankpw  9532  rankss  9538  ranksn  9543  rankuni2  9544  rankun  9545  rankpr  9546  rankop  9547  rankeq0  9550  rankr1b  9553  djuun  9615  dju1dif  9859  isfin4p1  10002  fin1a2lem4  10090  fin1a2lem6  10092  hsmexlem6  10118  dcomex  10134  axdc3lem4  10140  canthp1lem2  10340  pwxpndom2  10352  rankcf  10464  grutsk  10509  axgroth3  10518  inaprc  10523  1lt2pi  10592  pnfxr  10960  mnfxr  10963  1nn  11914  uzrdg0i  13607  axdc4uzlem  13631  ccat2s1p2  14265  ccat2s1p2OLD  14267  wrdl3s3  14605  infcvgaux1i  15497  0bits  16074  sadcf  16088  prmreclem6  16550  fnpr2ob  17186  setcepi  17719  setc2obas  17725  setc2ohom  17726  cat1  17728  smndex1mnd  18464  smndex1id  18465  pwmnd  18491  grpss  18512  psgnunilem2  19018  psgnprfval2  19046  efgi0  19241  efgi1  19242  vrgpf  19289  vrgpinv  19290  frgpuptinv  19292  frgpup2  19297  frgpnabllem1  19389  dmdprdpr  19567  dprdpr  19568  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  leordtval2  22271  xpstopnlem1  22868  xpstopnlem2  22870  ptcmp  23117  tsmsfbas  23187  zcld  23882  sszcld  23886  abscncfALT  23993  iimulcn  24007  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  cnstrcvs  24210  cncvs  24214  dveflem  25048  ftc1  25111  efopnlem2  25717  cxpcn3  25806  efrlim  26024  structvtxval  27294  usgrexmplef  27529  wwlks2onv  28219  elwwlks2ons3im  28220  umgrwwlks2on  28223  konigsberglem4  28520  hhshsslem2  29531  nonbooli  29914  nmopadjlei  30351  cshw1s2  31134  fzto1st  31272  cyc2fv1  31290  cyc3fv1  31306  cyc3fv2  31307  cyc3evpm  31319  xrge0iifhmeo  31788  dya2iocbrsiga  32142  dya2icobrsiga  32143  fib0  32266  fib1  32267  coinflippvt  32351  prodfzo03  32483  circlevma  32522  circlemethhgt  32523  hgt750lemg  32534  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgt  32543  bnj97  32746  bnj553  32778  bnj966  32824  bnj1442  32929  subfacp1lem2a  33042  subfacp1lem5  33046  erdszelem5  33057  erdszelem8  33060  ex-sategoelel12  33289  rankeq1o  34400  0hf  34406  onint1  34565  bj-0eltag  35095  bj-minftyccb  35323  finxpreclem4  35492  fdc  35830  reheibor  35924  0prjspnlem  40381  0prjspnrel  40385  pw2f1ocnv  40775  comptiunov2i  41203  clsk1indlem4  41543  clsk1indlem1  41544  mnuprdlem3  41781  sucidALTVD  42379  sucidALT  42380  sucidVD  42381  rfcnpre1  42451  eliuniincex  42548  iocopn  42948  icoopn  42953  islptre  43050  cnrefiisplem  43260  icccncfext  43318  fourierdlem103  43640  fourierdlem104  43641  iooborel  43780  sprsymrelfo  44837  sbgoldbo  45127  0even  45377  2even  45379  2zrngamgm  45385  zlmodzxzldeplem3  45731  rrx2pxel  45945  rrx2pyel  45946  rrx2linesl  45977  2sphere0  45984  i0oii  46101  io1ii  46102