Theorem eleqtrri 2477

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-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 2408	. 2 |- B = C
4	1, 3	eleqtri 2476	1 |- A e. C

Syntax hints:   = wceq 1649   e. wcel 1721

This theorem is referenced by:  3eltr4i  2483  opi1  4390  opi2  4391  seqomlem3  6668  oneo  6783  nnneo  6853  0elixp  7052  ac6sfi  7310  tz9.13  7673  rankval  7698  rankid  7715  ssrankr1  7717  rankel  7721  rankval3  7722  rankpw  7725  rankss  7731  ranksn  7736  rankuni2  7737  rankun  7738  rankpr  7739  rankop  7740  rankeq0  7743  rankr1b  7746  fin1a2lem4  8239  fin1a2lem6  8241  hsmexlem6  8267  dcomex  8283  axdc3lem4  8289  canthp1lem2  8484  pwxpndom2  8496  rankcf  8608  grutsk  8653  axgroth3  8662  inaprc  8667  1lt2pi  8738  1nn  9967  pnfxr  10669  mnfxr  10670  uzrdg0i  11254  axdc4uzlem  11276  eqs1  11716  infcvgaux1i  12591  0bits  12906  sadcf  12920  prmreclem6  13244  xpsfrnel2  13745  setcepi  14198  grpss  14781  efgi0  15307  efgi1  15308  vrgpf  15355  vrgpinv  15356  frgpuptinv  15358  frgpup2  15363  frgpnabllem1  15439  dmdprdpr  15562  dprdpr  15563  leordtval2  17230  xpstopnlem1  17794  xpstopnlem2  17796  ptcmp  18042  tsmsfbas  18110  zcld  18797  sszcld  18801  abscncfALT  18903  iimulcn  18916  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  dveflem  19816  ftc1  19879  efopnlem2  20501  cxpcn3  20585  efrlim  20761  usgraex0elv  21368  usgraex1elv  21369  usgraex2elv  21370  usgraex3elv  21371  wlkntrllem1  21512  konigsberg  21662  hhshsslem2  22721  nonbooli  23106  nmopadjlei  23544  xrge0iifhmeo  24275  dya2iocbrsiga  24578  dya2icobrsiga  24579  coinflippvt  24695  subfacp1lem2a  24819  subfacp1lem5  24823  erdszelem5  24834  erdszelem8  24837  wfrlem14  25483  wfrlem16  25485  rankeq1o  26016  0hf  26022  onint1  26103  fdc  26339  reheibor  26438  pw2f1ocnv  26998  psgnunilem2  27286  rfcnpre1  27557  usgra2pthspth  28035  usgra2wlkspthlem2  28037  el2wlkonotlem  28059  usg2wlkonot  28080  usg2wotspth  28081  sucidALTVD  28691  sucidALT  28692  sucidVD  28693  bnj97  28943  bnj553  28975  bnj966  29021  bnj1442  29124

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400