Theorem eqeltrri 2837

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

Syntax hints:   = wceq 1539   ∈ 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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  3eltr3i  2852  zfrep4  5221  p0ex  5308  pp0ex  5310  ord3ex  5311  zfpair  5345  epse  5573  unex  7605  fvresex  7811  opabex3  7819  abexssex  7822  abexex  7823  oprabrexex2  7830  seqomlem3  8292  1on  8318  2on  8320  inf0  9388  scottexs  9654  kardex  9661  infxpenlem  9778  r1om  10009  cfon  10020  fin23lem16  10100  fin1a2lem6  10170  hsmexlem5  10195  brdom7disj  10296  brdom6disj  10297  1lt2pi  10670  0cn  10976  resubcli  11292  0reALT  11327  1nn  11993  10nn  12462  numsucc  12486  nummac  12491  unirnioo  13190  ioorebas  13192  fz0to4untppr  13368  om2uzrani  13681  uzrdg0i  13688  hashunlei  14149  cats1fvn  14580  trclubi  14716  4sqlem19  16673  dec2dvds  16773  mod2xnegi  16781  modsubi  16782  gcdi  16783  isstruct2  16859  grppropstr  18605  nn0srg  20677  ltbval  21253  sn0topon  22157  indistop  22161  indisuni  22162  indistps2  22171  indistps2ALT  22174  restbas  22318  leordtval2  22372  iocpnfordt  22375  icomnfordt  22376  iooordt  22377  reordt  22378  dis1stc  22659  ptcmpfi  22973  ustfn  23362  ustn0  23381  retopbas  23933  blssioo  23967  xrtgioo  23978  zcld  23985  cnperf  23992  retopconn  24001  iimulcn  24110  rembl  24713  mbfdm  24799  ismbf  24801  mbf0  24807  bddiblnc  25015  abelthlem9  25608  advlog  25818  advlogexp  25819  2irrexpq  25894  cxpcn3  25910  loglesqrt  25920  log2ub  26108  ppi1i  26326  cht2  26330  cht3  26331  bpos1lem  26439  lgslem4  26457  vmadivsum  26639  log2sumbnd  26701  selberg2  26708  selbergr  26725  iscgrg  26882  ishpg  27129  ax5seglem7  27312  h2hva  29345  h2hsm  29346  h2hnm  29347  norm-ii-i  29508  hhshsslem2  29639  shincli  29733  chincli  29831  lnophdi  30373  imaelshi  30429  rnelshi  30430  bdophdi  30468  dfdec100  31153  dpadd2  31193  dpmul  31196  dpmul4  31197  nn0omnd  31554  nn0archi  31556  znfermltl  31571  ccfldextrr  31732  lmatfvlem  31774  rmulccn  31887  rrhre  31980  sigaex  32087  br2base  32245  sxbrsigalem3  32248  carsgclctunlem3  32296  sitmcl  32327  rpsqrtcn  32582  hgt750lem  32640  hgt750lem2  32641  afsval  32660  kur14lem7  33183  retopsconn  33220  satfvsuclem1  33330  fmlasuc0  33355  nogt01o  33908  hfuni  34495  neibastop2lem  34558  onint1  34647  topdifinffinlem  35527  poimirlem9  35795  poimirlem28  35814  poimirlem30  35816  poimirlem32  35818  ftc1cnnc  35858  cncfres  35932  lineset  37759  lautset  38103  pautsetN  38119  tendoset  38780  decpmulnc  40322  decpmul  40323  areaquad  41054  finonex  41068  sblpnf  41935  lhe4.4ex1a  41954  fourierdlem62  43716  fourierdlem76  43730  65537prm  45039  11gbo  45238  bgoldbtbndlem1  45268  seppcld  46234