Theorem eqeltrri 2831

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

Syntax hints:   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  3eltr3i  2846  zfrep4  5236  p0ex  5327  pp0ex  5329  ord3ex  5330  zfpair  5364  moabex  5404  epse  5604  unexOLD  7688  fvresex  7902  opabex3  7909  abexssex  7912  abexex  7913  oprabrexex2  7920  seqomlem3  8381  1on  8407  2on  8408  inf0  9528  scottexs  9797  kardex  9804  infxpenlem  9921  r1om  10151  cfon  10163  fin23lem16  10243  fin1a2lem6  10313  hsmexlem5  10338  brdom7disj  10439  brdom6disj  10440  1lt2pi  10814  0cn  11122  resubcli  11441  0reALT  11476  1nn  12154  10nn  12621  numsucc  12645  nummac  12650  unirnioo  13363  ioorebas  13365  om2uzrani  13873  uzrdg0i  13880  hashunlei  14346  cats1fvn  14779  trclubi  14917  4sqlem19  16889  dec2dvds  16989  mod2xnegi  16997  modsubi  16998  gcdi  16999  isstruct2  17074  grppropstr  18881  nn0srg  21390  fermltlchr  21482  ltbval  21996  sn0topon  22940  indistop  22944  indisuni  22945  indistps2  22954  indistps2ALT  22956  restbas  23100  leordtval2  23154  iocpnfordt  23157  icomnfordt  23158  iooordt  23159  reordt  23160  dis1stc  23441  ptcmpfi  23755  ustfn  24144  ustn0  24163  retopbas  24702  blssioo  24737  xrtgioo  24749  zcld  24756  cnperf  24763  retopconn  24772  iimulcnOLD  24889  rembl  25495  mbfdm  25581  ismbf  25583  mbf0  25589  bddiblnc  25797  abelthlem9  26404  advlog  26617  advlogexp  26618  2irrexpq  26694  cxpcn3  26712  loglesqrt  26725  log2ub  26913  ppi1i  27132  cht2  27136  cht3  27137  bpos1lem  27247  lgslem4  27265  vmadivsum  27447  log2sumbnd  27509  selberg2  27516  selbergr  27533  nogt01o  27662  mulsproplem9  28093  1n0s  28308  n0sfincut  28315  2nns  28376  iscgrg  28533  ishpg  28780  ax5seglem7  28957  h2hva  30998  h2hsm  30999  h2hnm  31000  norm-ii-i  31161  hhshsslem2  31292  shincli  31386  chincli  31484  lnophdi  32026  imaelshi  32082  rnelshi  32083  bdophdi  32121  dfdec100  32860  dpadd2  32940  dpmul  32943  dpmul4  32944  nn0omnd  33374  nn0archi  33377  znfermltl  33396  ccfldextrr  33752  lmatfvlem  33921  rrhre  34127  sigaex  34216  br2base  34375  sxbrsigalem3  34378  carsgclctunlem3  34426  sitmcl  34457  rpsqrtcn  34699  hgt750lem  34757  hgt750lem2  34758  afsval  34777  kur14lem7  35355  retopsconn  35392  satfvsuclem1  35502  fmlasuc0  35527  hfuni  36327  neibastop2lem  36503  onint1  36592  bj-snfromadj  37188  topdifinffinlem  37491  poimirlem9  37769  poimirlem28  37788  poimirlem30  37790  poimirlem32  37792  ftc1cnnc  37832  cncfres  37905  lineset  39937  lautset  40281  pautsetN  40297  tendoset  40958  decpmulnc  42484  decpmul  42485  areaquad  43400  0no  43618  finonex  43637  sblpnf  44493  lhe4.4ex1a  44512  fourierdlem62  46354  fourierdlem76  46368  lamberte  47076  65537prm  47764  11gbo  47963  bgoldbtbndlem1  47993  seppcld  49117