Theorem eleqtrri 2828

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

Syntax hints:   = wceq 1534   ∈ wcel 2100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2721  df-clel 2806

This theorem is referenced by:  3eltr4i  2842  vex  3476  vexOLD  3477  opi1  5476  opi2  5477  frrlem14  8318  wfrlem14OLD  8356  wfrlem16OLD  8358  seqomlem3  8486  nlim2  8524  oneo  8615  nnneo  8689  0elixp  8962  ac6sfi  9323  tz9.13  9835  rankval  9860  rankid  9877  ssrankr1  9879  rankel  9883  rankval3  9884  rankpw  9887  rankss  9893  ranksn  9898  rankuni2  9899  rankun  9900  rankpr  9901  rankop  9902  rankeq0  9905  rankr1b  9908  djuun  9970  dju1dif  10217  isfin4p1  10359  fin1a2lem4  10447  fin1a2lem6  10449  hsmexlem6  10475  dcomex  10491  axdc3lem4  10497  canthp1lem2  10697  pwxpndom2  10709  rankcf  10821  grutsk  10866  axgroth3  10875  inaprc  10880  1lt2pi  10949  pnfxr  11319  mnfxr  11322  1nn  12279  uzrdg0i  13984  axdc4uzlem  14008  ccat2s1p2  14651  wrdl3s3  14984  infcvgaux1i  15874  0bits  16452  sadcf  16466  prmreclem6  16936  fnpr2ob  17586  setcepi  18123  setc2obas  18129  setc2ohom  18130  cat1  18132  smndex1mnd  18913  smndex1id  18914  pwmnd  18940  grpss  18962  psgnunilem2  19505  psgnprfval2  19533  efgi0  19730  efgi1  19731  vrgpf  19778  vrgpinv  19779  frgpuptinv  19781  frgpup2  19786  frgpnabllem1  19883  dmdprdpr  20061  dprdpr  20062  pzriprnglem7  21489  pzriprnglem13  21495  pzriprng1ALT  21498  m2detleiblem3  22622  m2detleiblem4  22623  m2detleib  22624  leordtval2  23207  xpstopnlem1  23804  xpstopnlem2  23806  ptcmp  24053  tsmsfbas  24123  zcld  24820  sszcld  24824  abscncfALT  24936  iimulcn  24952  iimulcnOLD  24953  icopnfhmeo  24959  iccpnfhmeo  24961  xrhmeo  24962  cnstrcvs  25159  cncvs  25163  dveflem  26002  ftc1  26068  efopnlem2  26681  cxpcn3  26773  efrlim  26994  efrlimOLD  26995  precsexlem11  28215  1nns  28320  structvtxval  28999  usgrexmplef  29237  wwlks2onv  29929  elwwlks2ons3im  29930  umgrwwlks2on  29933  konigsberglem4  30230  hhshsslem2  31243  nonbooli  31626  nmopadjlei  32063  cshw1s2  32872  fzto1st  33041  cyc2fv1  33059  cyc3fv1  33075  cyc3fv2  33076  cyc3evpm  33088  1arithidom  33475  zringpid  33490  xrge0iifhmeo  33827  dya2iocbrsiga  34185  dya2icobrsiga  34186  fib0  34309  fib1  34310  coinflippvt  34394  prodfzo03  34525  circlevma  34564  circlemethhgt  34565  hgt750lemg  34576  hgt750lemb  34578  hgt750lema  34579  hgt750leme  34580  tgoldbachgtde  34582  tgoldbachgt  34585  bnj97  34787  bnj553  34819  bnj966  34865  bnj1442  34970  subfacp1lem2a  35093  subfacp1lem5  35097  erdszelem5  35108  erdszelem8  35111  ex-sategoelel12  35340  rankeq1o  36080  0hf  36086  onint1  36247  bj-0eltag  36770  bj-minftyccb  37017  finxpreclem4  37186  fdc  37531  reheibor  37625  0prjspnlem  42388  0prjspnrel  42392  pw2f1ocnv  42807  onexoegt  43021  2omomeqom  43081  omnord1ex  43082  oege2  43085  oenord1ex  43093  oenord1  43094  oaomoencom  43095  oenassex  43096  comptiunov2i  43485  clsk1indlem4  43823  clsk1indlem1  43824  mnuprdlem3  44060  sucidALTVD  44658  sucidALT  44659  sucidVD  44660  rfcnpre1  44730  eliuniincex  44822  iocopn  45249  icoopn  45254  islptre  45351  cnrefiisplem  45561  icccncfext  45619  fourierdlem103  45941  fourierdlem104  45942  iooborel  46083  upwordnul  46610  upwordsing  46614  sprsymrelfo  47180  sbgoldbo  47470  0even  47736  2even  47738  2zrngamgm  47744  zlmodzxzldeplem3  48007  rrx2pxel  48221  rrx2pyel  48222  rrx2linesl  48253  2sphere0  48260  i0oii  48375  io1ii  48376