Theorem eleqtrri 2838

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

Syntax hints:   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  3eltr4i  2852  vex  3435  opi1  5408  opi2  5409  frrlem14  8239  seqomlem3  8381  nlim2  8415  oneo  8506  nnneo  8581  0elixp  8867  ac6sfi  9184  tz9.13  9706  rankval  9731  rankid  9748  ssrankr1  9750  rankel  9754  rankval3  9755  rankpw  9758  rankss  9764  ranksn  9769  rankuni2  9770  rankun  9771  rankpr  9772  rankop  9773  rankeq0  9776  rankr1b  9779  djuun  9841  dju1dif  10086  isfin4p1  10228  fin1a2lem4  10316  fin1a2lem6  10318  hsmexlem6  10344  dcomex  10360  axdc3lem4  10366  canthp1lem2  10567  pwxpndom2  10579  rankcf  10691  grutsk  10736  axgroth3  10745  inaprc  10750  1lt2pi  10819  pnfxr  11190  mnfxr  11193  1nn  12176  uzrdg0i  13912  axdc4uzlem  13936  ccat2s1p2  14584  wrdl3s3  14915  infcvgaux1i  15813  0bits  16399  sadcf  16413  prmreclem6  16883  fnpr2ob  17513  setcepi  18046  setc2obas  18052  setc2ohom  18053  cat1  18055  smndex1mnd  18872  smndex1id  18873  pwmnd  18899  grpss  18921  psgnunilem2  19461  psgnprfval2  19489  efgi0  19686  efgi1  19687  vrgpf  19734  vrgpinv  19735  frgpuptinv  19737  frgpup2  19742  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  pzriprnglem7  21462  pzriprnglem13  21468  pzriprng1ALT  21471  m2detleiblem3  22612  m2detleiblem4  22613  m2detleib  22614  leordtval2  23195  xpstopnlem1  23792  xpstopnlem2  23794  ptcmp  24041  tsmsfbas  24111  zcld  24797  sszcld  24801  abscncfALT  24909  iimulcn  24923  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  cnstrcvs  25126  cncvs  25130  dveflem  25964  ftc1  26027  efopnlem2  26639  cxpcn3  26730  efrlim  26951  precsexlem11  28227  1nns  28359  structvtxval  29108  usgrexmplef  29346  wwlks2onv  30039  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  konigsberglem4  30343  hhshsslem2  31357  nonbooli  31740  nmopadjlei  32177  cshw1s2  33039  fzto1st  33184  cyc2fv1  33202  cyc3fv1  33218  cyc3fv2  33219  cyc3evpm  33231  1arithidom  33620  zringpid  33635  vieta  33764  xrge0iifhmeo  34120  dya2iocbrsiga  34459  dya2icobrsiga  34460  fib0  34583  fib1  34584  coinflippvt  34669  prodfzo03  34787  circlevma  34826  circlemethhgt  34827  hgt750lemg  34838  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  tgoldbachgt  34847  bnj97  35048  bnj553  35080  bnj966  35126  bnj1442  35231  fineqvnttrclse  35305  fineqvinfep  35306  subfacp1lem2a  35408  subfacp1lem5  35412  erdszelem5  35423  erdszelem8  35426  ex-sategoelel12  35655  rankeq1o  36399  0hf  36405  onint1  36677  regsfromunir1  36768  bj-0eltag  37331  bj-minftyccb  37585  finxpreclem4  37756  fdc  38112  reheibor  38206  0prjspnlem  43073  0prjspnrel  43077  pw2f1ocnv  43482  onexoegt  43689  2omomeqom  43748  omnord1ex  43749  oege2  43752  oenord1ex  43760  oenord1  43761  oaomoencom  43762  oenassex  43763  comptiunov2i  44150  clsk1indlem4  44488  clsk1indlem1  44489  mnuprdlem3  44718  sucidALTVD  45313  sucidALT  45314  sucidVD  45315  wfaxnul  45440  wfaxinf2  45445  nregmodellem  45460  rfcnpre1  45467  eliuniincex  45556  iocopn  45965  icoopn  45970  islptre  46064  cnrefiisplem  46272  icccncfext  46330  fourierdlem103  46652  fourierdlem104  46653  iooborel  46794  sprsymrelfo  47972  sbgoldbo  48278  stgr1  48452  isubgr3stgrlem7  48463  gpg3kgrtriexlem5  48578  pglem  48582  grlimedgnedg  48622  0even  48728  2even  48730  2zrngamgm  48736  zlmodzxzldeplem3  48993  rrx2pxel  49202  rrx2pyel  49203  rrx2linesl  49234  2sphere0  49241  i0oii  49410  io1ii  49411  setc1onsubc  50092