Theorem eleqtrri 2860

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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

This theorem is used by:  3eltr4i  2874  vex  3455  opi1  5437  opi2  5438  frrlem14  8317  seqomlem3  8462  nlim2  8498  oneo  8589  nnneo  8664  0elixp  8957  ac6sfi  9275  tz9.13  9798  rankval  9825  rankid  9845  ssrankr1  9847  rankel  9851  rankval3  9853  rankpw  9856  rankss  9863  ranksn  9868  rankuni2  9869  rankun  9870  rankpr  9871  rankop  9872  rankeq0  9877  rankr1b  9881  0hf  9917  djuun  10007  dju1dif  10251  isfin4p1  10393  fin1a2lem4  10481  fin1a2lem6  10483  hsmexlem6  10509  dcomex  10525  axdc3lem4  10531  canthp1lem2  10738  pwxpndom2  10750  rankcf  10862  grutsk  10907  axgroth3  10916  inaprc  10921  1lt2pi  10990  pnfxr  11363  mnfxr  11366  1nn  12346  uzrdg0i  14102  axdc4uzlem  14126  ccat2s1p2  14778  s3rex  15101  wrdl3s3  15115  infcvgaux1i  16026  0bits  16609  sadcf  16623  prmreclem6  17099  fnpr2ob  17730  setcepi  18263  setc2obas  18269  setc2ohom  18270  cat1  18272  smndex1mnd  19109  smndex1id  19110  pwmnd  19143  grpss  19165  psgnunilem2  19709  psgnprfval2  19737  efgi0  19934  efgi1  19935  vrgpf  19982  vrgpinv  19983  frgpuptinv  19985  frgpup2  19990  frgpnabllem1  20087  dmdprdpr  20265  dprdpr  20266  pzriprnglem7  21793  pzriprnglem13  21799  pzriprng1ALT  21802  m2detleiblem3  22944  m2detleiblem4  22945  m2detleib  22946  leordtval2  23530  xpstopnlem1  24128  xpstopnlem2  24130  ptcmp  24377  tsmsfbas  24447  zcld  25133  sszcld  25137  abscncfALT  25245  iimulcn  25259  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  cnstrcvs  25462  cncvs  25466  dveflem  26299  ftc1  26362  efopnlem2  26985  cxpcn3  27076  efrlim  27297  precsexlem11  28603  1nns  28735  structvtxval  29599  usgrexmplef  29840  wwlks2onv  30542  elwwlks2ons3im  30543  usgrwwlks2on  30547  umgrwwlks2on  30548  konigsberglem4  30856  hhshsslem2  31870  nonbooli  32253  nmopadjlei  32690  cshw1s2  33521  fzto1st  33664  cyc2fv1  33682  cyc3fv1  33698  cyc3fv2  33699  cyc3evpm  33711  1arithidom  34069  zringpid  34084  vieta  34212  xrge0iifhmeo  34568  dya2iocbrsiga  34907  dya2icobrsiga  34908  fib0  35031  fib1  35032  coinflippvt  35117  prodfzo03  35232  circlevma  35271  circlemethhgt  35272  hgt750lemg  35283  hgt750lemb  35285  hgt750lema  35286  hgt750leme  35287  tgoldbachgtde  35289  tgoldbachgt  35292  bnj97  35496  bnj553  35528  bnj966  35574  bnj1442  35679  fineqvnttrclse  35792  fineqvinfep  35793  subfacp1lem2a  35945  subfacp1lem5  35949  erdszelem5  35960  erdszelem8  35963  ex-sategoelel12  36192  rankeq1o  36932  onint1  37237  regsfromunir1  37328  bj-0eltag  37891  bj-minftyccb  38146  finxpreclem4  38317  fdc  38679  reheibor  38773  0prjspnlem  43662  0prjspnrel  43663  pw2f1ocnv  44043  onexoegt  44245  2omomeqom  44304  omnord1ex  44305  oege2  44308  oenord1ex  44316  oenord1  44317  oaomoencom  44318  oenassex  44319  comptiunov2i  44705  clsk1indlem4  45043  clsk1indlem1  45044  mnuprdlem3  45257  sucidALTVD  45851  sucidALT  45852  sucidVD  45853  wfaxnul  45985  wfaxinf2  45990  nregmodellem  46005  rfcnpre1  46035  eliuniincex  46123  iocopn  46531  icoopn  46536  islptre  46630  cnrefiisplem  46838  icccncfext  46896  fourierdlem103  47218  fourierdlem104  47219  iooborel  47360  tannpoly  47939  sprsymrelfo  48578  sbgoldbo  48884  stgr1  49058  isubgr3stgrlem7  49069  gpg3kgrtriexlem5  49184  pglem  49188  grlimedgnedg  49228  0even  49333  2even  49335  2zrngamgm  49341  zlmodzxzldeplem3  49613  rrx2pxel  49822  rrx2pyel  49823  rrx2linesl  49854  2sphere0  49861  i0oii  50027  io1ii  50028  setc1onsubc  50709