Theorem eqeltrri 2830

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

Hypotheses

Ref	Expression
eqeltrri.1	⊢ 𝐴 = 𝐵
eqeltrri.2	⊢ 𝐴 ∈ 𝐶

Assertion

Ref	Expression
eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrri.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2741	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2829	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  3eltr3i  2845  zfrep4  5296  p0ex  5382  pp0ex  5384  ord3ex  5385  zfpair  5419  epse  5659  unex  7735  fvresex  7948  opabex3  7956  abexssex  7959  abexex  7960  oprabrexex2  7967  seqomlem3  8454  1on  8480  2on  8482  inf0  9618  scottexs  9884  kardex  9891  infxpenlem  10010  r1om  10241  cfon  10252  fin23lem16  10332  fin1a2lem6  10402  hsmexlem5  10427  brdom7disj  10528  brdom6disj  10529  1lt2pi  10902  0cn  11208  resubcli  11524  0reALT  11559  1nn  12225  10nn  12695  numsucc  12719  nummac  12724  unirnioo  13428  ioorebas  13430  fz0to4untppr  13606  om2uzrani  13919  uzrdg0i  13926  hashunlei  14387  cats1fvn  14811  trclubi  14945  4sqlem19  16898  dec2dvds  16998  mod2xnegi  17006  modsubi  17007  gcdi  17008  isstruct2  17084  grppropstr  18841  nn0srg  21021  ltbval  21604  sn0topon  22508  indistop  22512  indisuni  22513  indistps2  22522  indistps2ALT  22525  restbas  22669  leordtval2  22723  iocpnfordt  22726  icomnfordt  22727  iooordt  22728  reordt  22729  dis1stc  23010  ptcmpfi  23324  ustfn  23713  ustn0  23732  retopbas  24284  blssioo  24318  xrtgioo  24329  zcld  24336  cnperf  24343  retopconn  24352  iimulcn  24461  rembl  25064  mbfdm  25150  ismbf  25152  mbf0  25158  bddiblnc  25366  abelthlem9  25959  advlog  26169  advlogexp  26170  2irrexpq  26246  cxpcn3  26263  loglesqrt  26273  log2ub  26461  ppi1i  26679  cht2  26683  cht3  26684  bpos1lem  26792  lgslem4  26810  vmadivsum  26992  log2sumbnd  27054  selberg2  27061  selbergr  27078  nogt01o  27206  mulsproplem9  27590  0n0s  27710  iscgrg  27801  ishpg  28048  ax5seglem7  28231  h2hva  30265  h2hsm  30266  h2hnm  30267  norm-ii-i  30428  hhshsslem2  30559  shincli  30653  chincli  30751  lnophdi  31293  imaelshi  31349  rnelshi  31350  bdophdi  31388  dfdec100  32074  dpadd2  32114  dpmul  32117  dpmul4  32118  nn0omnd  32501  nn0archi  32503  fermltlchr  32523  znfermltl  32524  ccfldextrr  32786  lmatfvlem  32864  rmulccn  32977  rrhre  33070  sigaex  33177  br2base  33337  sxbrsigalem3  33340  carsgclctunlem3  33388  sitmcl  33419  rpsqrtcn  33674  hgt750lem  33732  hgt750lem2  33733  afsval  33752  kur14lem7  34272  retopsconn  34309  satfvsuclem1  34419  fmlasuc0  34444  hfuni  35225  neibastop2lem  35331  onint1  35420  bj-snfromadj  36011  topdifinffinlem  36314  poimirlem9  36583  poimirlem28  36602  poimirlem30  36604  poimirlem32  36606  ftc1cnnc  36646  cncfres  36719  lineset  38695  lautset  39039  pautsetN  39055  tendoset  39716  decpmulnc  41281  decpmul  41282  areaquad  42047  0no  42268  finonex  42287  sblpnf  43151  lhe4.4ex1a  43170  fourierdlem62  44963  fourierdlem76  44977  65537prm  46323  11gbo  46522  bgoldbtbndlem1  46552  seppcld  47640