Theorem eleqtrri 2828

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

Syntax hints:   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806

This theorem is referenced by:  3eltr4i  2842  vex  3474  vexOLD  3475  opi1  5464  opi2  5465  frrlem14  8298  wfrlem14OLD  8336  wfrlem16OLD  8338  seqomlem3  8466  nlim2  8504  oneo  8595  nnneo  8669  0elixp  8941  ac6sfi  9305  tz9.13  9808  rankval  9833  rankid  9850  ssrankr1  9852  rankel  9856  rankval3  9857  rankpw  9860  rankss  9866  ranksn  9871  rankuni2  9872  rankun  9873  rankpr  9874  rankop  9875  rankeq0  9878  rankr1b  9881  djuun  9943  dju1dif  10189  isfin4p1  10332  fin1a2lem4  10420  fin1a2lem6  10422  hsmexlem6  10448  dcomex  10464  axdc3lem4  10470  canthp1lem2  10670  pwxpndom2  10682  rankcf  10794  grutsk  10839  axgroth3  10848  inaprc  10853  1lt2pi  10922  pnfxr  11292  mnfxr  11295  1nn  12247  uzrdg0i  13950  axdc4uzlem  13974  ccat2s1p2  14606  wrdl3s3  14939  infcvgaux1i  15829  0bits  16407  sadcf  16421  prmreclem6  16883  fnpr2ob  17533  setcepi  18070  setc2obas  18076  setc2ohom  18077  cat1  18079  smndex1mnd  18855  smndex1id  18856  pwmnd  18882  grpss  18904  psgnunilem2  19443  psgnprfval2  19471  efgi0  19668  efgi1  19669  vrgpf  19716  vrgpinv  19717  frgpuptinv  19719  frgpup2  19724  frgpnabllem1  19821  dmdprdpr  19999  dprdpr  20000  pzriprnglem7  21406  pzriprnglem13  21412  pzriprng1ALT  21415  m2detleiblem3  22524  m2detleiblem4  22525  m2detleib  22526  leordtval2  23109  xpstopnlem1  23706  xpstopnlem2  23708  ptcmp  23955  tsmsfbas  24025  zcld  24722  sszcld  24726  abscncfALT  24838  iimulcn  24854  iimulcnOLD  24855  icopnfhmeo  24861  iccpnfhmeo  24863  xrhmeo  24864  cnstrcvs  25061  cncvs  25065  dveflem  25904  ftc1  25970  efopnlem2  26584  cxpcn3  26676  efrlim  26894  efrlimOLD  26895  precsexlem11  28108  1nns  28208  structvtxval  28827  usgrexmplef  29065  wwlks2onv  29757  elwwlks2ons3im  29758  umgrwwlks2on  29761  konigsberglem4  30058  hhshsslem2  31071  nonbooli  31454  nmopadjlei  31891  cshw1s2  32675  fzto1st  32818  cyc2fv1  32836  cyc3fv1  32852  cyc3fv2  32853  cyc3evpm  32865  xrge0iifhmeo  33531  dya2iocbrsiga  33889  dya2icobrsiga  33890  fib0  34013  fib1  34014  coinflippvt  34098  prodfzo03  34229  circlevma  34268  circlemethhgt  34269  hgt750lemg  34280  hgt750lemb  34282  hgt750lema  34283  hgt750leme  34284  tgoldbachgtde  34286  tgoldbachgt  34289  bnj97  34491  bnj553  34523  bnj966  34569  bnj1442  34674  subfacp1lem2a  34784  subfacp1lem5  34788  erdszelem5  34799  erdszelem8  34802  ex-sategoelel12  35031  rankeq1o  35761  0hf  35767  onint1  35927  bj-0eltag  36451  bj-minftyccb  36698  finxpreclem4  36867  fdc  37212  reheibor  37306  0prjspnlem  42041  0prjspnrel  42045  pw2f1ocnv  42452  onexoegt  42666  2omomeqom  42726  omnord1ex  42727  oege2  42730  oenord1ex  42738  oenord1  42739  oaomoencom  42740  oenassex  42741  comptiunov2i  43130  clsk1indlem4  43468  clsk1indlem1  43469  mnuprdlem3  43705  sucidALTVD  44303  sucidALT  44304  sucidVD  44305  rfcnpre1  44375  eliuniincex  44469  iocopn  44899  icoopn  44904  islptre  45001  cnrefiisplem  45211  icccncfext  45269  fourierdlem103  45591  fourierdlem104  45592  iooborel  45733  upwordnul  46260  upwordsing  46264  sprsymrelfo  46831  sbgoldbo  47121  0even  47293  2even  47295  2zrngamgm  47301  zlmodzxzldeplem3  47564  rrx2pxel  47778  rrx2pyel  47779  rrx2linesl  47810  2sphere0  47817  i0oii  47932  io1ii  47933