Theorem eqeltrri 2825

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  3eltr3i  2840  zfrep4  5248  p0ex  5339  pp0ex  5341  ord3ex  5342  zfpair  5376  epse  5620  unexOLD  7721  fvresex  7938  opabex3  7946  abexssex  7949  abexex  7950  oprabrexex2  7957  seqomlem3  8420  1on  8446  2on  8447  inf0  9574  scottexs  9840  kardex  9847  infxpenlem  9966  r1om  10196  cfon  10208  fin23lem16  10288  fin1a2lem6  10358  hsmexlem5  10383  brdom7disj  10484  brdom6disj  10485  1lt2pi  10858  0cn  11166  resubcli  11484  0reALT  11519  1nn  12197  10nn  12665  numsucc  12689  nummac  12694  unirnioo  13410  ioorebas  13412  om2uzrani  13917  uzrdg0i  13924  hashunlei  14390  cats1fvn  14824  trclubi  14962  4sqlem19  16934  dec2dvds  17034  mod2xnegi  17042  modsubi  17043  gcdi  17044  isstruct2  17119  grppropstr  18885  nn0srg  21354  fermltlchr  21439  ltbval  21950  sn0topon  22885  indistop  22889  indisuni  22890  indistps2  22899  indistps2ALT  22901  restbas  23045  leordtval2  23099  iocpnfordt  23102  icomnfordt  23103  iooordt  23104  reordt  23105  dis1stc  23386  ptcmpfi  23700  ustfn  24089  ustn0  24108  retopbas  24648  blssioo  24683  xrtgioo  24695  zcld  24702  cnperf  24709  retopconn  24718  iimulcnOLD  24835  rembl  25441  mbfdm  25527  ismbf  25529  mbf0  25535  bddiblnc  25743  abelthlem9  26350  advlog  26563  advlogexp  26564  2irrexpq  26640  cxpcn3  26658  loglesqrt  26671  log2ub  26859  ppi1i  27078  cht2  27082  cht3  27083  bpos1lem  27193  lgslem4  27211  vmadivsum  27393  log2sumbnd  27455  selberg2  27462  selbergr  27479  nogt01o  27608  mulsproplem9  28027  1n0s  28240  n0sfincut  28246  2nns  28304  iscgrg  28439  ishpg  28686  ax5seglem7  28862  h2hva  30903  h2hsm  30904  h2hnm  30905  norm-ii-i  31066  hhshsslem2  31197  shincli  31291  chincli  31389  lnophdi  31931  imaelshi  31987  rnelshi  31988  bdophdi  32026  dfdec100  32755  dpadd2  32830  dpmul  32833  dpmul4  32834  nn0omnd  33316  nn0archi  33318  znfermltl  33337  ccfldextrr  33642  lmatfvlem  33805  rrhre  34011  sigaex  34100  br2base  34260  sxbrsigalem3  34263  carsgclctunlem3  34311  sitmcl  34342  rpsqrtcn  34584  hgt750lem  34642  hgt750lem2  34643  afsval  34662  kur14lem7  35199  retopsconn  35236  satfvsuclem1  35346  fmlasuc0  35371  hfuni  36172  neibastop2lem  36348  onint1  36437  bj-snfromadj  37032  topdifinffinlem  37335  poimirlem9  37623  poimirlem28  37642  poimirlem30  37644  poimirlem32  37646  ftc1cnnc  37686  cncfres  37759  lineset  39732  lautset  40076  pautsetN  40092  tendoset  40753  decpmulnc  42275  decpmul  42276  areaquad  43205  0no  43424  finonex  43443  sblpnf  44299  lhe4.4ex1a  44318  fourierdlem62  46166  fourierdlem76  46180  lamberte  46889  65537prm  47577  11gbo  47776  bgoldbtbndlem1  47806  seppcld  48918