Theorem eqeltrri 2829

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 2740	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2828	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 2702

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

This theorem is referenced by:  3eltr3i  2844  zfrep4  5258  p0ex  5344  pp0ex  5346  ord3ex  5347  zfpair  5381  epse  5621  unex  7685  fvresex  7897  opabex3  7905  abexssex  7908  abexex  7909  oprabrexex2  7916  seqomlem3  8403  1on  8429  2on  8431  inf0  9566  scottexs  9832  kardex  9839  infxpenlem  9958  r1om  10189  cfon  10200  fin23lem16  10280  fin1a2lem6  10350  hsmexlem5  10375  brdom7disj  10476  brdom6disj  10477  1lt2pi  10850  0cn  11156  resubcli  11472  0reALT  11507  1nn  12173  10nn  12643  numsucc  12667  nummac  12672  unirnioo  13376  ioorebas  13378  fz0to4untppr  13554  om2uzrani  13867  uzrdg0i  13874  hashunlei  14335  cats1fvn  14759  trclubi  14893  4sqlem19  16846  dec2dvds  16946  mod2xnegi  16954  modsubi  16955  gcdi  16956  isstruct2  17032  grppropstr  18781  nn0srg  20904  ltbval  21481  sn0topon  22385  indistop  22389  indisuni  22390  indistps2  22399  indistps2ALT  22402  restbas  22546  leordtval2  22600  iocpnfordt  22603  icomnfordt  22604  iooordt  22605  reordt  22606  dis1stc  22887  ptcmpfi  23201  ustfn  23590  ustn0  23609  retopbas  24161  blssioo  24195  xrtgioo  24206  zcld  24213  cnperf  24220  retopconn  24229  iimulcn  24338  rembl  24941  mbfdm  25027  ismbf  25029  mbf0  25035  bddiblnc  25243  abelthlem9  25836  advlog  26046  advlogexp  26047  2irrexpq  26122  cxpcn3  26138  loglesqrt  26148  log2ub  26336  ppi1i  26554  cht2  26558  cht3  26559  bpos1lem  26667  lgslem4  26685  vmadivsum  26867  log2sumbnd  26929  selberg2  26936  selbergr  26953  nogt01o  27081  mulsproplem10  27431  iscgrg  27517  ishpg  27764  ax5seglem7  27947  h2hva  29979  h2hsm  29980  h2hnm  29981  norm-ii-i  30142  hhshsslem2  30273  shincli  30367  chincli  30465  lnophdi  31007  imaelshi  31063  rnelshi  31064  bdophdi  31102  dfdec100  31796  dpadd2  31836  dpmul  31839  dpmul4  31840  nn0omnd  32208  nn0archi  32210  fermltlchr  32226  znfermltl  32227  ccfldextrr  32424  lmatfvlem  32485  rmulccn  32598  rrhre  32691  sigaex  32798  br2base  32958  sxbrsigalem3  32961  carsgclctunlem3  33009  sitmcl  33040  rpsqrtcn  33295  hgt750lem  33353  hgt750lem2  33354  afsval  33373  kur14lem7  33893  retopsconn  33930  satfvsuclem1  34040  fmlasuc0  34065  hfuni  34845  neibastop2lem  34908  onint1  34997  bj-snfromadj  35588  topdifinffinlem  35891  poimirlem9  36160  poimirlem28  36179  poimirlem30  36181  poimirlem32  36183  ftc1cnnc  36223  cncfres  36297  lineset  38274  lautset  38618  pautsetN  38634  tendoset  39295  decpmulnc  40859  decpmul  40860  areaquad  41608  0no  41829  finonex  41848  sblpnf  42712  lhe4.4ex1a  42731  fourierdlem62  44529  fourierdlem76  44543  65537prm  45888  11gbo  46087  bgoldbtbndlem1  46117  seppcld  47082