Theorem eleqtrri 2832

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

Syntax hints:   = wceq 1541   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  3eltr4i  2846  vex  3478  vexOLD  3479  opi1  5467  opi2  5468  frrlem14  8280  wfrlem14OLD  8318  wfrlem16OLD  8320  seqomlem3  8448  nlim2  8486  oneo  8577  nnneo  8650  0elixp  8919  ac6sfi  9283  tz9.13  9782  rankval  9807  rankid  9824  ssrankr1  9826  rankel  9830  rankval3  9831  rankpw  9834  rankss  9840  ranksn  9845  rankuni2  9846  rankun  9847  rankpr  9848  rankop  9849  rankeq0  9852  rankr1b  9855  djuun  9917  dju1dif  10163  isfin4p1  10306  fin1a2lem4  10394  fin1a2lem6  10396  hsmexlem6  10422  dcomex  10438  axdc3lem4  10444  canthp1lem2  10644  pwxpndom2  10656  rankcf  10768  grutsk  10813  axgroth3  10822  inaprc  10827  1lt2pi  10896  pnfxr  11264  mnfxr  11267  1nn  12219  uzrdg0i  13920  axdc4uzlem  13944  ccat2s1p2  14576  wrdl3s3  14909  infcvgaux1i  15799  0bits  16376  sadcf  16390  prmreclem6  16850  fnpr2ob  17500  setcepi  18034  setc2obas  18040  setc2ohom  18041  cat1  18043  smndex1mnd  18787  smndex1id  18788  pwmnd  18814  grpss  18836  psgnunilem2  19357  psgnprfval2  19385  efgi0  19582  efgi1  19583  vrgpf  19630  vrgpinv  19631  frgpuptinv  19633  frgpup2  19638  frgpnabllem1  19735  dmdprdpr  19913  dprdpr  19914  m2detleiblem3  22122  m2detleiblem4  22123  m2detleib  22124  leordtval2  22707  xpstopnlem1  23304  xpstopnlem2  23306  ptcmp  23553  tsmsfbas  23623  zcld  24320  sszcld  24324  abscncfALT  24431  iimulcn  24445  icopnfhmeo  24450  iccpnfhmeo  24452  xrhmeo  24453  cnstrcvs  24648  cncvs  24652  dveflem  25487  ftc1  25550  efopnlem2  26156  cxpcn3  26245  efrlim  26463  precsexlem11  27652  structvtxval  28270  usgrexmplef  28505  wwlks2onv  29196  elwwlks2ons3im  29197  umgrwwlks2on  29200  konigsberglem4  29497  hhshsslem2  30508  nonbooli  30891  nmopadjlei  31328  cshw1s2  32111  fzto1st  32249  cyc2fv1  32267  cyc3fv1  32283  cyc3fv2  32284  cyc3evpm  32296  xrge0iifhmeo  32904  dya2iocbrsiga  33262  dya2icobrsiga  33263  fib0  33386  fib1  33387  coinflippvt  33471  prodfzo03  33603  circlevma  33642  circlemethhgt  33643  hgt750lemg  33654  hgt750lemb  33656  hgt750lema  33657  hgt750leme  33658  tgoldbachgtde  33660  tgoldbachgt  33663  bnj97  33865  bnj553  33897  bnj966  33943  bnj1442  34048  subfacp1lem2a  34159  subfacp1lem5  34163  erdszelem5  34174  erdszelem8  34177  ex-sategoelel12  34406  rankeq1o  35131  0hf  35137  gg-iimulcn  35157  onint1  35322  bj-0eltag  35847  bj-minftyccb  36094  finxpreclem4  36263  fdc  36601  reheibor  36695  0prjspnlem  41361  0prjspnrel  41365  pw2f1ocnv  41761  onexoegt  41978  2omomeqom  42038  omnord1ex  42039  oege2  42042  oenord1ex  42050  oenord1  42051  oaomoencom  42052  oenassex  42053  comptiunov2i  42442  clsk1indlem4  42780  clsk1indlem1  42781  mnuprdlem3  43018  sucidALTVD  43616  sucidALT  43617  sucidVD  43618  rfcnpre1  43688  eliuniincex  43783  iocopn  44219  icoopn  44224  islptre  44321  cnrefiisplem  44531  icccncfext  44589  fourierdlem103  44911  fourierdlem104  44912  iooborel  45053  upwordnul  45580  upwordsing  45584  sprsymrelfo  46151  sbgoldbo  46441  0even  46782  2even  46784  2zrngamgm  46790  zlmodzxzldeplem3  47136  rrx2pxel  47350  rrx2pyel  47351  rrx2linesl  47382  2sphere0  47389  i0oii  47505  io1ii  47506