Theorem eqeltrri 2698

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrri	|- B e. C

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 |- A = B
2	1	eqcomi 2631	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltri 2697	1 |- B 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:  3eltr3i  2713  zfrep4  4779  p0ex  4853  pp0ex  4855  ord3ex  4856  zfpair  4904  epse  5097  unex  6956  fvresex  7139  abrexexOLD  7142  opabex3  7146  abexssex  7149  abrexex2OLD  7150  abexex  7151  oprabrexex2  7158  seqomlem3  7547  inf0  8518  scottexs  8750  kardex  8757  infxpenlem  8836  r1om  9066  cfon  9077  fin23lem16  9157  fin1a2lem6  9227  hsmexlem5  9252  brdom7disj  9353  brdom6disj  9354  1lt2pi  9727  0cn  10032  resubcli  10343  0reALT  10378  1nn  11031  10nn  11514  numsucc  11549  nummac  11558  unirnioo  12273  ioorebas  12275  fz0to4untppr  12442  om2uzrani  12751  uzrdg0i  12758  hashunlei  13212  cats1fvn  13603  trclubi  13735  trclubiOLD  13736  4sqlem19  15667  dec2dvds  15767  mod2xnegi  15775  modsubi  15776  gcdi  15777  isstruct2  15867  grppropstr  17439  ltbval  19471  nn0srg  19816  sn0topon  20802  indistop  20806  indisuni  20807  indistps2  20816  indistps2ALT  20818  restbas  20962  leordtval2  21016  iocpnfordt  21019  icomnfordt  21020  iooordt  21021  reordt  21022  dis1stc  21302  ptcmpfi  21616  ustfn  22005  ustn0  22024  retopbas  22564  blssioo  22598  xrtgioo  22609  zcld  22616  cnperf  22623  retopconn  22632  iimulcn  22737  rembl  23308  mbfdm  23395  ismbf  23397  abelthlem9  24194  advlog  24400  advlogexp  24401  cxpcn3  24489  loglesqrt  24499  log2ub  24676  ppi1i  24894  cht2  24898  cht3  24899  bpos1lem  25007  lgslem4  25025  vmadivsum  25171  log2sumbnd  25233  selberg2  25240  selbergr  25257  iscgrg  25407  ishpg  25651  ax5seglem7  25815  fusgrfis  26222  h2hva  27831  h2hsm  27832  h2hnm  27833  norm-ii-i  27994  hhshsslem2  28125  shincli  28221  chincli  28319  lnophdi  28861  imaelshi  28917  rnelshi  28918  bdophdi  28956  dfdec100  29576  dpadd2  29618  dpmul  29621  dpmul4  29622  nn0omnd  29841  nn0archi  29843  lmatfvlem  29881  rmulccn  29974  rrhre  30065  sigaex  30172  br2base  30331  sxbrsigalem3  30334  carsgclctunlem3  30382  sitmcl  30413  rpsqrtcn  30671  hgt750lem  30729  hgt750lem2  30730  afsval  30749  kur14lem7  31194  retopsconn  31231  hfuni  32291  neibastop2lem  32355  onint1  32448  topdifinffinlem  33195  poimirlem9  33418  poimirlem28  33437  poimirlem30  33439  poimirlem32  33441  0mbf  33455  bddiblnc  33480  ftc1cnnc  33484  cncfres  33564  lineset  35024  lautset  35368  pautsetN  35384  tendoset  36047  areaquad  37802  sblpnf  38509  lhe4.4ex1a  38528  fourierdlem62  40385  fourierdlem76  40399  65537prm  41488  11gbo  41663  bgoldbtbndlem1  41693