Theorem eqeltrri 2831

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 2742	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2830	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  3eltr3i  2846  zfrep4  5297  p0ex  5383  pp0ex  5385  ord3ex  5386  zfpair  5420  epse  5660  unex  7733  fvresex  7946  opabex3  7954  abexssex  7957  abexex  7958  oprabrexex2  7965  seqomlem3  8452  1on  8478  2on  8480  inf0  9616  scottexs  9882  kardex  9889  infxpenlem  10008  r1om  10239  cfon  10250  fin23lem16  10330  fin1a2lem6  10400  hsmexlem5  10425  brdom7disj  10526  brdom6disj  10527  1lt2pi  10900  0cn  11206  resubcli  11522  0reALT  11557  1nn  12223  10nn  12693  numsucc  12717  nummac  12722  unirnioo  13426  ioorebas  13428  fz0to4untppr  13604  om2uzrani  13917  uzrdg0i  13924  hashunlei  14385  cats1fvn  14809  trclubi  14943  4sqlem19  16896  dec2dvds  16996  mod2xnegi  17004  modsubi  17005  gcdi  17006  isstruct2  17082  grppropstr  18839  nn0srg  21015  ltbval  21598  sn0topon  22501  indistop  22505  indisuni  22506  indistps2  22515  indistps2ALT  22518  restbas  22662  leordtval2  22716  iocpnfordt  22719  icomnfordt  22720  iooordt  22721  reordt  22722  dis1stc  23003  ptcmpfi  23317  ustfn  23706  ustn0  23725  retopbas  24277  blssioo  24311  xrtgioo  24322  zcld  24329  cnperf  24336  retopconn  24345  iimulcn  24454  rembl  25057  mbfdm  25143  ismbf  25145  mbf0  25151  bddiblnc  25359  abelthlem9  25952  advlog  26162  advlogexp  26163  2irrexpq  26239  cxpcn3  26256  loglesqrt  26266  log2ub  26454  ppi1i  26672  cht2  26676  cht3  26677  bpos1lem  26785  lgslem4  26803  vmadivsum  26985  log2sumbnd  27047  selberg2  27054  selbergr  27071  nogt01o  27199  mulsproplem9  27580  iscgrg  27763  ishpg  28010  ax5seglem7  28193  h2hva  30227  h2hsm  30228  h2hnm  30229  norm-ii-i  30390  hhshsslem2  30521  shincli  30615  chincli  30713  lnophdi  31255  imaelshi  31311  rnelshi  31312  bdophdi  31350  dfdec100  32036  dpadd2  32076  dpmul  32079  dpmul4  32080  nn0omnd  32460  nn0archi  32462  fermltlchr  32478  znfermltl  32479  ccfldextrr  32727  lmatfvlem  32795  rmulccn  32908  rrhre  33001  sigaex  33108  br2base  33268  sxbrsigalem3  33271  carsgclctunlem3  33319  sitmcl  33350  rpsqrtcn  33605  hgt750lem  33663  hgt750lem2  33664  afsval  33683  kur14lem7  34203  retopsconn  34240  satfvsuclem1  34350  fmlasuc0  34375  hfuni  35156  neibastop2lem  35245  onint1  35334  bj-snfromadj  35925  topdifinffinlem  36228  poimirlem9  36497  poimirlem28  36516  poimirlem30  36518  poimirlem32  36520  ftc1cnnc  36560  cncfres  36633  lineset  38609  lautset  38953  pautsetN  38969  tendoset  39630  decpmulnc  41199  decpmul  41200  areaquad  41965  0no  42186  finonex  42205  sblpnf  43069  lhe4.4ex1a  43088  fourierdlem62  44884  fourierdlem76  44898  65537prm  46244  11gbo  46443  bgoldbtbndlem1  46473  seppcld  47562