Theorem eqeltrri 2834

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr3i  2849  zfrep4  5242  p0ex  5333  pp0ex  5335  ord3ex  5336  zfpair  5370  moabex  5415  epse  5616  unexOLD  7702  fvresex  7916  opabex3  7923  abexssex  7926  abexex  7927  oprabrexex2  7934  seqomlem3  8395  1on  8421  2on  8422  inf0  9544  scottexs  9813  kardex  9820  infxpenlem  9937  r1om  10167  cfon  10179  fin23lem16  10259  fin1a2lem6  10329  hsmexlem5  10354  brdom7disj  10455  brdom6disj  10456  1lt2pi  10830  0cn  11138  resubcli  11457  0reALT  11492  1nn  12170  10nn  12637  numsucc  12661  nummac  12666  unirnioo  13379  ioorebas  13381  om2uzrani  13889  uzrdg0i  13896  hashunlei  14362  cats1fvn  14795  trclubi  14933  4sqlem19  16905  dec2dvds  17005  mod2xnegi  17013  modsubi  17014  gcdi  17015  isstruct2  17090  smndex1gbas  18841  smndex1gid  18843  smndex1igid  18845  grppropstr  18900  nn0srg  21409  fermltlchr  21501  ltbval  22015  sn0topon  22959  indistop  22963  indisuni  22964  indistps2  22973  indistps2ALT  22975  restbas  23119  leordtval2  23173  iocpnfordt  23176  icomnfordt  23177  iooordt  23178  reordt  23179  dis1stc  23460  ptcmpfi  23774  ustfn  24163  ustn0  24182  retopbas  24721  blssioo  24756  xrtgioo  24768  zcld  24775  cnperf  24782  retopconn  24791  iimulcnOLD  24908  rembl  25514  mbfdm  25600  ismbf  25602  mbf0  25608  bddiblnc  25816  abelthlem9  26423  advlog  26636  advlogexp  26637  2irrexpq  26713  cxpcn3  26731  loglesqrt  26744  log2ub  26932  ppi1i  27151  cht2  27155  cht3  27156  bpos1lem  27266  lgslem4  27284  vmadivsum  27466  log2sumbnd  27528  selberg2  27535  selbergr  27552  nogt01o  27681  mulsproplem9  28137  1n0s  28361  n0fincut  28368  2nns  28431  istrkg2ld  28549  iscgrg  28602  ishpg  28849  ax5seglem7  29026  h2hva  31068  h2hsm  31069  h2hnm  31070  norm-ii-i  31231  hhshsslem2  31362  shincli  31456  chincli  31554  lnophdi  32096  imaelshi  32152  rnelshi  32153  bdophdi  32191  padct  32814  dfdec100  32928  dpadd2  33008  dpmul  33011  dpmul4  33012  nn0omnd  33443  nn0archi  33446  znfermltl  33465  ccfldextrr  33830  lmatfvlem  33999  rrhre  34205  sigaex  34294  br2base  34453  sxbrsigalem3  34456  carsgclctunlem3  34504  sitmcl  34535  rpsqrtcn  34777  hgt750lem  34835  hgt750lem2  34836  afsval  34855  kur14lem7  35434  retopsconn  35471  satfvsuclem1  35581  fmlasuc0  35606  hfuni  36406  neibastop2lem  36582  onint1  36671  bj-snfromadj  37319  topdifinffinlem  37629  poimirlem9  37909  poimirlem28  37928  poimirlem30  37930  poimirlem32  37932  ftc1cnnc  37972  cncfres  38045  lineset  40143  lautset  40487  pautsetN  40503  tendoset  41164  decpmulnc  42686  decpmul  42687  areaquad  43602  0fno  43820  finonex  43839  sblpnf  44695  lhe4.4ex1a  44714  fourierdlem62  46555  fourierdlem76  46569  lamberte  47277  65537prm  47965  11gbo  48164  bgoldbtbndlem1  48194  seppcld  49318