Theorem eleqtrri 2862

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

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

This theorem is used by:  3eltr4i  2876  vex  3457  opi1  5440  opi2  5441  frrlem14  8328  seqomlem3  8473  nlim2  8509  oneo  8600  nnneo  8675  0elixp  8968  ac6sfi  9286  tz9.13  9808  rankval  9835  rankid  9855  ssrankr1  9857  rankel  9861  rankval3  9863  rankpw  9866  rankss  9873  ranksn  9878  rankuni2  9879  rankun  9880  rankpr  9881  rankop  9882  rankeq0  9887  rankr1b  9891  0hf  9927  djuun  10017  dju1dif  10261  isfin4p1  10403  fin1a2lem4  10491  fin1a2lem6  10493  hsmexlem6  10519  dcomex  10535  axdc3lem4  10541  canthp1lem2  10748  pwxpndom2  10760  rankcf  10872  grutsk  10917  axgroth3  10926  inaprc  10931  1lt2pi  11000  pnfxr  11373  mnfxr  11376  1nn  12356  uzrdg0i  14112  axdc4uzlem  14136  ccat2s1p2  14789  s3rex  15113  wrdl3s3  15127  infcvgaux1i  16038  0bits  16621  sadcf  16635  prmreclem6  17111  fnpr2ob  17742  setcepi  18275  setc2obas  18281  setc2ohom  18282  cat1  18284  smndex1mnd  19121  smndex1id  19122  pwmnd  19155  grpss  19177  psgnunilem2  19721  psgnprfval2  19749  efgi0  19946  efgi1  19947  vrgpf  19994  vrgpinv  19995  frgpuptinv  19997  frgpup2  20002  frgpnabllem1  20099  dmdprdpr  20277  dprdpr  20278  pzriprnglem7  21805  pzriprnglem13  21811  pzriprng1ALT  21814  m2detleiblem3  22956  m2detleiblem4  22957  m2detleib  22958  leordtval2  23542  xpstopnlem1  24140  xpstopnlem2  24142  ptcmp  24389  tsmsfbas  24459  zcld  25145  sszcld  25149  abscncfALT  25257  iimulcn  25271  icopnfhmeo  25276  iccpnfhmeo  25278  xrhmeo  25279  cnstrcvs  25474  cncvs  25478  dveflem  26311  ftc1  26374  efopnlem2  26997  cxpcn3  27088  efrlim  27309  precsexlem11  28615  1nns  28747  structvtxval  29611  usgrexmplef  29852  wwlks2onv  30554  elwwlks2ons3im  30555  usgrwwlks2on  30559  umgrwwlks2on  30560  konigsberglem4  30868  hhshsslem2  31882  nonbooli  32265  nmopadjlei  32702  cshw1s2  33574  fzto1st  33717  cyc2fv1  33735  cyc3fv1  33751  cyc3fv2  33752  cyc3evpm  33764  1arithidom  34122  zringpid  34137  vieta  34265  xrge0iifhmeo  34621  dya2iocbrsiga  34960  dya2icobrsiga  34961  fib0  35084  fib1  35085  coinflippvt  35170  prodfzo03  35285  circlevma  35324  circlemethhgt  35325  hgt750lemg  35336  hgt750lemb  35338  hgt750lema  35339  hgt750leme  35340  tgoldbachgtde  35342  tgoldbachgt  35345  bnj97  35549  bnj553  35581  bnj966  35627  bnj1442  35732  fineqvnttrclse  35863  fineqvinfep  35864  subfacp1lem2a  36066  subfacp1lem5  36070  erdszelem5  36081  erdszelem8  36084  ex-sategoelel12  36313  rankeq1o  37059  onint1  37364  regsfromunir1  37455  bj-0eltag  38018  bj-minftyccb  38286  finxpreclem4  38457  fdc  38819  reheibor  38913  0prjspnlem  43802  0prjspnrel  43803  pw2f1ocnv  44184  onexoegt  44386  2omomeqom  44445  omnord1ex  44446  oege2  44449  oenord1ex  44457  oenord1  44458  oaomoencom  44459  oenassex  44460  comptiunov2i  44846  clsk1indlem4  45184  clsk1indlem1  45185  mnuprdlem3  45398  sucidALTVD  45991  sucidALT  45992  sucidVD  45993  wfaxnul  46125  wfaxinf2  46130  nregmodellem  46145  rfcnpre1  46175  eliuniincex  46263  iocopn  46671  icoopn  46676  islptre  46770  cnrefiisplem  46978  icccncfext  47036  fourierdlem103  47358  fourierdlem104  47359  iooborel  47500  tannpoly  48079  sprsymrelfo  48718  sbgoldbo  49024  stgr1  49198  isubgr3stgrlem7  49209  gpg3kgrtriexlem5  49324  pglem  49328  grlimedgnedg  49368  0even  49473  2even  49475  2zrngamgm  49481  zlmodzxzldeplem3  49753  rrx2pxel  49962  rrx2pyel  49963  2sphere0  50001  i0oii  50173  io1ii  50174  setc1onsubc  50879  parcatid2  50902  parcatid  50903  parswapprop  50916  par2hom  50918  par2diag  50919  fuconuniqlem  50920  fuconuniqvalslem  50922