Theorem eqeltrri 2828

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

Syntax hints:   = wceq 1543   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  3eltr3i  2843  zfrep4  5174  p0ex  5262  pp0ex  5264  ord3ex  5265  zfpair  5299  epse  5519  unex  7509  fvresex  7711  opabex3  7718  abexssex  7721  abexex  7722  oprabrexex2  7729  seqomlem3  8166  inf0  9214  scottexs  9468  kardex  9475  infxpenlem  9592  r1om  9823  cfon  9834  fin23lem16  9914  fin1a2lem6  9984  hsmexlem5  10009  brdom7disj  10110  brdom6disj  10111  1lt2pi  10484  0cn  10790  resubcli  11105  0reALT  11140  1nn  11806  10nn  12274  numsucc  12298  nummac  12303  unirnioo  13002  ioorebas  13004  fz0to4untppr  13180  om2uzrani  13490  uzrdg0i  13497  hashunlei  13957  cats1fvn  14388  trclubi  14524  4sqlem19  16479  dec2dvds  16579  mod2xnegi  16587  modsubi  16588  gcdi  16589  isstruct2  16676  grppropstr  18338  nn0srg  20387  ltbval  20954  sn0topon  21849  indistop  21853  indisuni  21854  indistps2  21863  indistps2ALT  21865  restbas  22009  leordtval2  22063  iocpnfordt  22066  icomnfordt  22067  iooordt  22068  reordt  22069  dis1stc  22350  ptcmpfi  22664  ustfn  23053  ustn0  23072  retopbas  23612  blssioo  23646  xrtgioo  23657  zcld  23664  cnperf  23671  retopconn  23680  iimulcn  23789  rembl  24391  mbfdm  24477  ismbf  24479  mbf0  24485  bddiblnc  24693  abelthlem9  25286  advlog  25496  advlogexp  25497  2irrexpq  25572  cxpcn3  25588  loglesqrt  25598  log2ub  25786  ppi1i  26004  cht2  26008  cht3  26009  bpos1lem  26117  lgslem4  26135  vmadivsum  26317  log2sumbnd  26379  selberg2  26386  selbergr  26403  iscgrg  26557  ishpg  26804  ax5seglem7  26980  h2hva  29009  h2hsm  29010  h2hnm  29011  norm-ii-i  29172  hhshsslem2  29303  shincli  29397  chincli  29495  lnophdi  30037  imaelshi  30093  rnelshi  30094  bdophdi  30132  dfdec100  30818  dpadd2  30858  dpmul  30861  dpmul4  30862  nn0omnd  31213  nn0archi  31215  znfermltl  31230  ccfldextrr  31391  lmatfvlem  31433  rmulccn  31546  rrhre  31637  sigaex  31744  br2base  31902  sxbrsigalem3  31905  carsgclctunlem3  31953  sitmcl  31984  rpsqrtcn  32239  hgt750lem  32297  hgt750lem2  32298  afsval  32317  kur14lem7  32841  retopsconn  32878  satfvsuclem1  32988  fmlasuc0  33013  nogt01o  33585  hfuni  34172  neibastop2lem  34235  onint1  34324  topdifinffinlem  35204  poimirlem9  35472  poimirlem28  35491  poimirlem30  35493  poimirlem32  35495  ftc1cnnc  35535  cncfres  35609  lineset  37438  lautset  37782  pautsetN  37798  tendoset  38459  decpmulnc  39963  decpmul  39964  areaquad  40691  sblpnf  41542  lhe4.4ex1a  41561  fourierdlem62  43327  fourierdlem76  43341  65537prm  44644  11gbo  44843  bgoldbtbndlem1  44873  seppcld  45839