Theorem eleqtrri 2863

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  3eltr4i  2877  vex  3458  opi1  5444  opi2  5445  frrlem14  8355  seqomlem3  8500  nlim2  8536  oneo  8627  nnneo  8702  0elixp  8995  ac6sfi  9313  tz9.13  9835  rankval  9862  rankid  9882  ssrankr1  9884  rankel  9888  rankval3  9890  rankpw  9893  rankss  9900  ranksn  9905  rankuni2  9906  rankun  9907  rankpr  9908  rankop  9909  rankeq0  9914  rankr1b  9918  0hf  9954  djuun  10044  dju1dif  10290  isfin4p1  10432  fin1a2lem4  10520  fin1a2lem6  10522  hsmexlem6  10548  dcomex  10564  axdc3lem4  10570  canthp1lem2  10777  pwxpndom2  10789  rankcf  10901  grutsk  10946  axgroth3  10955  inaprc  10960  1lt2pi  11029  pnfxr  11402  mnfxr  11405  1nn  12386  uzrdg0i  14142  axdc4uzlem  14166  ccat2s1p2  14820  s3rex  15144  wrdl3s3  15158  infcvgaux1i  16070  0bits  16653  sadcf  16667  prmreclem6  17143  fnpr2ob  17780  setcepi  18313  setc2obas  18319  setc2ohom  18320  cat1  18322  smndex1mnd  19159  smndex1id  19160  pwmnd  19193  grpss  19215  psgnunilem2  19760  psgnprfval2  19788  efgi0  19985  efgi1  19986  vrgpf  20033  vrgpinv  20034  frgpuptinv  20036  frgpup2  20041  frgpnabllem1  20138  dmdprdpr  20316  dprdpr  20317  pzriprnglem7  21848  pzriprnglem13  21854  pzriprng1ALT  21857  m2detleiblem3  22999  m2detleiblem4  23000  m2detleib  23001  leordtval2  23585  xpstopnlem1  24183  xpstopnlem2  24185  ptcmp  24432  tsmsfbas  24502  zcld  25188  sszcld  25192  abscncfALT  25300  iimulcn  25314  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  cnstrcvs  25517  cncvs  25521  dveflem  26354  ftc1  26417  efopnlem2  27042  cxpcn3  27133  efrlim  27354  precsexlem11  28660  1nns  28792  structvtxval  29656  usgrexmplef  29897  wwlks2onv  30599  elwwlks2ons3im  30600  usgrwwlks2on  30604  umgrwwlks2on  30605  konigsberglem4  30913  hhshsslem2  31927  nonbooli  32310  nmopadjlei  32747  cshw1s2  33617  fzto1st  33763  cyc2fv1  33781  cyc3fv1  33797  cyc3fv2  33798  cyc3evpm  33810  1arithidom  34173  zringpid  34187  vieta  34323  xrge0iifhmeo  34679  dya2iocbrsiga  35018  dya2icobrsiga  35019  fib0  35142  fib1  35143  coinflippvt  35228  prodfzo03  35343  circlevma  35382  circlemethhgt  35383  hgt750lemg  35394  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  tgoldbachgtde  35400  tgoldbachgt  35403  bnj97  35607  bnj553  35639  bnj966  35685  bnj1442  35790  eqsucidi  35831  8olt9o  35914  7olt9o  35915  6olt9o  35916  5olt9o  35917  4olt9o  35918  3olt9o  35919  2olt9o  35920  1olt9o  35921  fineqvnttrclse  35933  fineqvinfep  35934  subfacp1lem2a  36153  subfacp1lem5  36157  erdszelem5  36168  erdszelem8  36171  ex-sategoelel12  36400  rankeq1o  37147  onint1  37452  regsfromunir1  37543  bj-0eltag  38106  bj-minftyccb  38414  finxpreclem4  38585  fdc  38945  reheibor  39039  0prjspnlem  43928  0prjspnrel  43929  pw2f1ocnv  44310  onexoegt  44507  2omomeqom  44566  omnord1ex  44567  oege2  44570  oenord1ex  44578  oenord1  44579  oaomoencom  44580  oenassex  44581  comptiunov2i  44967  clsk1indlem4  45305  clsk1indlem1  45306  mnuprdlem3  45519  sucidALTVD  46112  sucidALT  46113  sucidVD  46114  wfaxnul  46250  wfaxinf2  46255  nregmodellem  46270  rfcnpre1  46310  eliuniincex  46397  iocopn  46805  icoopn  46810  islptre  46904  cnrefiisplem  47112  icccncfext  47170  fourierdlem103  47492  fourierdlem104  47493  iooborel  47634  tannpoly  48213  sprsymrelfo  48852  sbgoldbo  49158  stgr1  49332  isubgr3stgrlem7  49343  gpg3kgrtriexlem5  49458  pglem  49462  grlimedgnedg  49502  0even  49607  2even  49609  2zrngamgm  49615  zlmodzxzldeplem3  49945  rrx2pxel  50154  rrx2pyel  50155  i0oii  50365  io1ii  50366  setc1onsubc  51071  parcatid2  51094  parcatid  51095  parswapprop  51108  par2hom  51110  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114