Theorem eqeltrri 2830

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 2829	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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

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

This theorem is referenced by:  3eltr3i  2845  zfrep4  5273  p0ex  5364  pp0ex  5366  ord3ex  5367  zfpair  5401  epse  5647  unexOLD  7747  fvresex  7966  opabex3  7974  abexssex  7977  abexex  7978  oprabrexex2  7985  seqomlem3  8474  1on  8500  2on  8502  inf0  9643  scottexs  9909  kardex  9916  infxpenlem  10035  r1om  10265  cfon  10277  fin23lem16  10357  fin1a2lem6  10427  hsmexlem5  10452  brdom7disj  10553  brdom6disj  10554  1lt2pi  10927  0cn  11235  resubcli  11553  0reALT  11588  1nn  12259  10nn  12732  numsucc  12756  nummac  12761  unirnioo  13471  ioorebas  13473  om2uzrani  13975  uzrdg0i  13982  hashunlei  14446  cats1fvn  14879  trclubi  15017  4sqlem19  16983  dec2dvds  17083  mod2xnegi  17091  modsubi  17092  gcdi  17093  isstruct2  17168  grppropstr  18940  nn0srg  21417  fermltlchr  21502  ltbval  22015  sn0topon  22952  indistop  22956  indisuni  22957  indistps2  22966  indistps2ALT  22968  restbas  23112  leordtval2  23166  iocpnfordt  23169  icomnfordt  23170  iooordt  23171  reordt  23172  dis1stc  23453  ptcmpfi  23767  ustfn  24156  ustn0  24175  retopbas  24717  blssioo  24752  xrtgioo  24764  zcld  24771  cnperf  24778  retopconn  24787  iimulcnOLD  24904  rembl  25511  mbfdm  25597  ismbf  25599  mbf0  25605  bddiblnc  25813  abelthlem9  26420  advlog  26632  advlogexp  26633  2irrexpq  26709  cxpcn3  26727  loglesqrt  26740  log2ub  26928  ppi1i  27147  cht2  27151  cht3  27152  bpos1lem  27262  lgslem4  27280  vmadivsum  27462  log2sumbnd  27524  selberg2  27531  selbergr  27548  nogt01o  27677  mulsproplem9  28086  1n0s  28287  2nns  28338  iscgrg  28456  ishpg  28703  ax5seglem7  28880  h2hva  30921  h2hsm  30922  h2hnm  30923  norm-ii-i  31084  hhshsslem2  31215  shincli  31309  chincli  31407  lnophdi  31949  imaelshi  32005  rnelshi  32006  bdophdi  32044  dfdec100  32772  dpadd2  32832  dpmul  32835  dpmul4  32836  nn0omnd  33308  nn0archi  33310  znfermltl  33329  ccfldextrr  33634  lmatfvlem  33773  rrhre  33981  sigaex  34070  br2base  34230  sxbrsigalem3  34233  carsgclctunlem3  34281  sitmcl  34312  rpsqrtcn  34567  hgt750lem  34625  hgt750lem2  34626  afsval  34645  kur14lem7  35176  retopsconn  35213  satfvsuclem1  35323  fmlasuc0  35348  hfuni  36144  neibastop2lem  36320  onint1  36409  bj-snfromadj  37004  topdifinffinlem  37307  poimirlem9  37595  poimirlem28  37614  poimirlem30  37616  poimirlem32  37618  ftc1cnnc  37658  cncfres  37731  lineset  39699  lautset  40043  pautsetN  40059  tendoset  40720  decpmulnc  42285  decpmul  42286  areaquad  43191  0no  43410  finonex  43429  sblpnf  44286  lhe4.4ex1a  44305  fourierdlem62  46140  fourierdlem76  46154  65537prm  47521  11gbo  47720  bgoldbtbndlem1  47750  seppcld  48787