Theorem eleqtrri 2516

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 2447	. 2 |- B = C
4	1, 3	eleqtri 2515	1 |- A e. C

Syntax hints:   = wceq 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439

This theorem is referenced by:  3eltr4i  2522  opi1  4562  opi2  4563  seqomlem3  6910  oneo  7023  nnneo  7093  0elixp  7297  ac6sfi  7559  tz9.13  8001  rankval  8026  rankid  8043  ssrankr1  8045  rankel  8049  rankval3  8050  rankpw  8053  rankss  8059  ranksn  8064  rankuni2  8065  rankun  8066  rankpr  8067  rankop  8068  rankeq0  8071  rankr1b  8074  fin1a2lem4  8575  fin1a2lem6  8577  hsmexlem6  8603  dcomex  8619  axdc3lem4  8625  canthp1lem2  8823  pwxpndom2  8835  rankcf  8947  grutsk  8992  axgroth3  9001  inaprc  9006  1lt2pi  9077  1nn  10336  pnfxr  11095  mnfxr  11097  uzrdg0i  11785  axdc4uzlem  11807  eqs1  12303  infcvgaux1i  13322  0bits  13638  sadcf  13652  prmreclem6  13985  xpsfrnel2  14506  setcepi  14959  grpss  15562  psgnunilem2  16004  psgnprfval2  16030  efgi0  16220  efgi1  16221  vrgpf  16268  vrgpinv  16269  frgpuptinv  16271  frgpup2  16276  frgpnabllem1  16354  dmdprdpr  16551  dprdpr  16552  m2detleiblem3  18438  m2detleiblem4  18439  m2detleib  18440  leordtval2  18819  xpstopnlem1  19385  xpstopnlem2  19387  ptcmp  19633  tsmsfbas  19701  zcld  20393  sszcld  20397  abscncfALT  20499  iimulcn  20513  icopnfhmeo  20518  iccpnfhmeo  20520  xrhmeo  20521  dveflem  21454  ftc1  21517  efopnlem2  22105  cxpcn3  22189  efrlim  22366  usgraex0elv  23317  usgraex1elv  23318  usgraex2elv  23319  usgraex3elv  23320  wlkntrllem1  23461  konigsberg  23611  hhshsslem2  24672  nonbooli  25057  nmopadjlei  25495  xrge0iifhmeo  26369  dya2iocbrsiga  26693  dya2icobrsiga  26694  fib0  26785  fib1  26786  coinflippvt  26870  signstfvn  26973  subfacp1lem2a  27071  subfacp1lem5  27075  erdszelem5  27086  erdszelem8  27089  wfrlem14  27740  wfrlem16  27742  rankeq1o  28212  0hf  28218  onint1  28298  fdc  28644  reheibor  28741  pw2f1ocnv  29389  rfcnpre1  29744  ccat2s1p2  30269  usgra2pthspth  30298  usgra2wlkspthlem2  30300  el2wlkonotlem  30384  usg2wlkonot  30405  usg2wotspth  30406  zlmodzxzldeplem3  31047  sucidALTVD  31609  sucidALT  31610  sucidVD  31611  bnj97  31862  bnj553  31894  bnj966  31940  bnj1442  32043  bj-0eltag  32474  bj-minftyccb  32551