Theorem eleqtrri 2864

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

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

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 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  3eltr4i  2878  vex  3461  opi1  5452  opi2  5453  frrlem14  8302  seqomlem3  8445  nlim2  8481  oneo  8572  nnneo  8647  0elixp  8933  ac6sfi  9251  tz9.13  9770  rankval  9795  rankid  9812  ssrankr1  9814  rankel  9818  rankval3  9819  rankpw  9822  rankss  9828  ranksn  9833  rankuni2  9834  rankun  9835  rankpr  9836  rankop  9837  rankeq0  9840  rankr1b  9843  djuun  9928  dju1dif  10172  isfin4p1  10314  fin1a2lem4  10402  fin1a2lem6  10404  hsmexlem6  10430  dcomex  10446  axdc3lem4  10452  canthp1lem2  10655  pwxpndom2  10667  rankcf  10779  grutsk  10824  axgroth3  10833  inaprc  10838  1lt2pi  10907  pnfxr  11280  mnfxr  11283  1nn  12261  uzrdg0i  14015  axdc4uzlem  14039  ccat2s1p2  14690  wrdl3s3  15025  infcvgaux1i  15936  0bits  16521  sadcf  16535  prmreclem6  17005  fnpr2ob  17636  setcepi  18169  setc2obas  18175  setc2ohom  18176  cat1  18178  smndex1mnd  19011  smndex1id  19012  pwmnd  19045  grpss  19067  psgnunilem2  19611  psgnprfval2  19639  efgi0  19836  efgi1  19837  vrgpf  19884  vrgpinv  19885  frgpuptinv  19887  frgpup2  19892  frgpnabllem1  19989  dmdprdpr  20167  dprdpr  20168  pzriprnglem7  21689  pzriprnglem13  21695  pzriprng1ALT  21698  m2detleiblem3  22838  m2detleiblem4  22839  m2detleib  22840  leordtval2  23421  xpstopnlem1  24019  xpstopnlem2  24021  ptcmp  24268  tsmsfbas  24338  zcld  25024  sszcld  25028  abscncfALT  25136  iimulcn  25150  icopnfhmeo  25155  iccpnfhmeo  25157  xrhmeo  25158  cnstrcvs  25353  cncvs  25357  dveflem  26191  ftc1  26254  efopnlem2  26875  cxpcn3  26966  efrlim  27187  precsexlem11  28463  1nns  28595  structvtxval  29428  usgrexmplef  29669  wwlks2onv  30371  elwwlks2ons3im  30372  usgrwwlks2on  30376  umgrwwlks2on  30377  konigsberglem4  30679  hhshsslem2  31693  nonbooli  32076  nmopadjlei  32513  cshw1s2  33346  fzto1st  33489  cyc2fv1  33507  cyc3fv1  33523  cyc3fv2  33524  cyc3evpm  33536  1arithidom  33893  zringpid  33908  vieta  34036  xrge0iifhmeo  34392  dya2iocbrsiga  34732  dya2icobrsiga  34733  fib0  34856  fib1  34857  coinflippvt  34942  prodfzo03  35057  circlevma  35096  circlemethhgt  35097  hgt750lemg  35108  hgt750lemb  35110  hgt750lema  35111  hgt750leme  35112  tgoldbachgtde  35114  tgoldbachgt  35117  bnj97  35321  bnj553  35353  bnj966  35399  bnj1442  35504  fineqvnttrclse  35596  fineqvinfep  35597  subfacp1lem2a  35711  subfacp1lem5  35715  erdszelem5  35726  erdszelem8  35729  ex-sategoelel12  35958  rankeq1o  36702  0hf  36708  onint1  37019  regsfromunir1  37110  bj-0eltag  37673  bj-minftyccb  37928  finxpreclem4  38099  fdc  38456  reheibor  38550  0prjspnlem  43415  0prjspnrel  43419  pw2f1ocnv  43824  onexoegt  44031  2omomeqom  44090  omnord1ex  44091  oege2  44094  oenord1ex  44102  oenord1  44103  oaomoencom  44104  oenassex  44105  comptiunov2i  44492  clsk1indlem4  44830  clsk1indlem1  44831  mnuprdlem3  45044  sucidALTVD  45638  sucidALT  45639  sucidVD  45640  wfaxnul  45765  wfaxinf2  45770  nregmodellem  45785  rfcnpre1  45799  eliuniincex  45887  iocopn  46296  icoopn  46301  islptre  46395  cnrefiisplem  46603  icccncfext  46661  fourierdlem103  46983  fourierdlem104  46984  iooborel  47125  sprsymrelfo  48306  sbgoldbo  48612  stgr1  48786  isubgr3stgrlem7  48797  gpg3kgrtriexlem5  48912  pglem  48916  grlimedgnedg  48956  0even  49061  2even  49063  2zrngamgm  49069  zlmodzxzldeplem3  49341  rrx2pxel  49550  rrx2pyel  49551  rrx2linesl  49582  2sphere0  49589  i0oii  49757  io1ii  49758  setc1onsubc  50439