Theorem eleqtrri 2700

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtrr.1	|- A e. B
eleqtrr.2	|- C = B

Assertion

Ref	Expression
eleqtrri	|- A e. C

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 |- A e. B
2		eleqtrr.2	. . 3 |- C = B
3	2	eqcomi 2631	. 2 |- B = C
4	1, 3	eleqtri 2699	1 |- A e. C

Syntax hints:   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  3eltr4i  2714  opi1  4937  opi2  4938  wfrlem14  7428  wfrlem16  7430  seqomlem3  7547  oneo  7661  nnneo  7731  0elixp  7939  ac6sfi  8204  tz9.13  8654  rankval  8679  rankid  8696  ssrankr1  8698  rankel  8702  rankval3  8703  rankpw  8706  rankss  8712  ranksn  8717  rankuni2  8718  rankun  8719  rankpr  8720  rankop  8721  rankeq0  8724  rankr1b  8727  fin1a2lem4  9225  fin1a2lem6  9227  hsmexlem6  9253  dcomex  9269  axdc3lem4  9275  canthp1lem2  9475  pwxpndom2  9487  rankcf  9599  grutsk  9644  axgroth3  9653  inaprc  9658  1lt2pi  9727  pnfxr  10092  mnfxr  10096  1nn  11031  uzrdg0i  12758  axdc4uzlem  12782  ccat2s1p2  13406  wrdl3s3  13705  infcvgaux1i  14589  0bits  15161  sadcf  15175  prmreclem6  15625  xpsfrnel2  16225  setcepi  16738  grpss  17440  psgnunilem2  17915  psgnprfval2  17943  efgi0  18133  efgi1  18134  vrgpf  18181  vrgpinv  18182  frgpuptinv  18184  frgpup2  18189  frgpnabllem1  18276  dmdprdpr  18448  dprdpr  18449  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  leordtval2  21016  xpstopnlem1  21612  xpstopnlem2  21614  ptcmp  21862  tsmsfbas  21931  zcld  22616  sszcld  22620  abscncfALT  22723  iimulcn  22737  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  cnstrcvs  22941  cncvs  22945  dveflem  23742  ftc1  23805  efopnlem2  24403  cxpcn3  24489  efrlim  24696  structvtxval  25910  usgrexmplef  26151  umgrwwlks2on  26850  konigsberglem4  27117  hhshsslem2  28125  nonbooli  28510  nmopadjlei  28947  fzto1st  29853  xrge0iifhmeo  29982  dya2iocbrsiga  30337  dya2icobrsiga  30338  fib0  30461  fib1  30462  coinflippvt  30546  signstfvn  30646  prodfzo03  30681  circlevma  30720  circlemethhgt  30721  hgt750lemg  30732  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  tgoldbachgt  30741  bnj97  30936  bnj553  30968  bnj966  31014  bnj1442  31117  subfacp1lem2a  31162  subfacp1lem5  31166  erdszelem5  31177  erdszelem8  31180  rankeq1o  32278  0hf  32284  onint1  32448  bj-0eltag  32966  bj-minftyccb  33112  finxpreclem4  33231  fdc  33541  reheibor  33638  pw2f1ocnv  37604  comptiunov2i  37998  corclrcl  37999  clsk1indlem4  38342  clsk1indlem1  38343  sucidALTVD  39106  sucidALT  39107  sucidVD  39108  rfcnpre1  39178  eliuniincex  39292  iocopn  39746  icoopn  39751  islptre  39851  cnrefiisplem  40055  icccncfext  40100  fourierdlem103  40426  fourierdlem104  40427  iooborel  40569  sbgoldbo  41675  sprsymrelfo  41747  0even  41931  2even  41933  2zrngamgm  41939  zlmodzxzldeplem3  42291