Theorem eqeltrri 2861

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

Syntax hints:   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  3eltr3i  2876  zfrep4  5245  p0ex  5343  pp0ex  5345  ord3ex  5346  zfpair  5380  moabex  5427  epse  5631  unexOLD  7730  fvresex  7943  opabex3  7950  abexssex  7953  abexex  7954  oprabrexex2  7961  seqomlem3  8425  1on  8452  2on  8453  inf0  9578  scottexs  9847  kardex  9854  infxpenlem  9971  r1om  10201  cfonOLD  10214  fin23lem16  10294  fin1a2lem6  10364  hsmexlem5  10389  brdom7disj  10490  brdom6disj  10491  1lt2pi  10865  0cn  11173  resubcli  11495  0reALT  11530  1nn  12223  10nn  12710  numsucc  12735  nummac  12740  unirnioo  13455  ioorebas  13457  om2uzrani  13967  uzrdg0i  13974  hashunlei  14440  cats1fvn  14873  trclubi  15011  sgnrn  15113  4sqlem19  17001  dec2dvds  17101  mod2xnegi  17109  modsubi  17110  gcdi  17111  isstruct2  17187  smndex1gbas  18938  smndex1gid  18940  smndex1igid  18942  grppropstr  18997  nn0srg  21491  fermltlchr  21583  ltbval  22098  sn0topon  23060  indistop  23064  indisuni  23065  indistps2  23074  indistps2ALT  23076  restbas  23220  leordtval2  23274  iocpnfordt  23277  icomnfordt  23278  iooordt  23279  reordt  23280  dis1stc  23561  ptcmpfi  23875  ustfn  24264  ustn0  24283  retopbas  24822  blssioo  24857  xrtgioo  24869  zcld  24876  cnperf  24883  retopconn  24892  rembl  25604  mbfdm  25690  ismbf  25692  mbf0  25698  bddiblnc  25906  abelthlem9  26505  advlog  26721  advlogexp  26722  2irrexpq  26798  cxpcn3  26815  loglesqrt  26828  log2ub  27016  ppi1i  27234  cht2  27238  cht3  27239  bpos1lem  27348  lgslem4  27366  vmadivsum  27548  log2sumbnd  27610  selberg2  27617  selbergr  27634  nogt01o  27762  mulsproplem9  28219  1n0s  28443  n0fincut  28450  2nns  28513  istrkg2ld  28631  iscgrg  28683  ishpg  28934  ax5seglem7  29138  h2hva  31179  h2hsm  31180  h2hnm  31181  norm-ii-i  31342  hhshsslem2  31473  shincli  31567  chincli  31665  lnophdi  32207  imaelshi  32263  rnelshi  32264  bdophdi  32302  padct  32922  dfdec100  33034  dpadd2  33089  dpmul  33092  dpmul4  33093  nn0omnd  33532  nn0archi  33535  znfermltl  33554  ccfldextrr  33945  lmatfvlem  34114  rrhre  34320  sigaex  34409  br2base  34568  sxbrsigalem3  34571  carsgclctunlem3  34619  sitmcl  34650  rpsqrtcn  34889  hgt750lem  34947  hgt750lem2  34948  afsval  34970  kur14lem7  35567  retopsconn  35604  satfvsuclem1  35714  fmlasuc0  35739  hfuni  36539  neibastop2lem  36725  onint1  36814  ttcid  36857  bj-snfromadj  37534  topdifinffinlem  37846  poimirlem9  38133  poimirlem28  38152  poimirlem30  38154  poimirlem32  38156  ftc1cnnc  38196  cncfres  38269  lineset  40367  lautset  40711  pautsetN  40727  tendoset  41388  decpmulnc  42901  decpmul  42902  areaquad  43798  0fno  44016  finonex  44035  sblpnf  44891  lhe4.4ex1a  44910  fourierdlem62  46747  fourierdlem76  46761  lamberte  47487  65537prm  48190  11gbo  48402  bgoldbtbndlem1  48432  seppcld  49556  setc1onsubc  50228