Theorem eqeltrri 2833

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 2832	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr3i  2848  zfrep4  5228  p0ex  5326  pp0ex  5328  ord3ex  5329  zfpair  5363  moabex  5410  epse  5613  unexOLD  7699  fvresex  7913  opabex3  7920  abexssex  7923  abexex  7924  oprabrexex2  7931  seqomlem3  8391  1on  8417  2on  8418  inf0  9542  scottexs  9811  kardex  9818  infxpenlem  9935  r1om  10165  cfon  10177  fin23lem16  10257  fin1a2lem6  10327  hsmexlem5  10352  brdom7disj  10453  brdom6disj  10454  1lt2pi  10828  0cn  11136  resubcli  11456  0reALT  11491  1nn  12185  10nn  12660  numsucc  12684  nummac  12689  unirnioo  13402  ioorebas  13404  om2uzrani  13914  uzrdg0i  13921  hashunlei  14387  cats1fvn  14820  trclubi  14958  4sqlem19  16934  dec2dvds  17034  mod2xnegi  17042  modsubi  17043  gcdi  17044  isstruct2  17119  smndex1gbas  18870  smndex1gid  18872  smndex1igid  18874  grppropstr  18929  nn0srg  21417  fermltlchr  21509  ltbval  22021  sn0topon  22963  indistop  22967  indisuni  22968  indistps2  22977  indistps2ALT  22979  restbas  23123  leordtval2  23177  iocpnfordt  23180  icomnfordt  23181  iooordt  23182  reordt  23183  dis1stc  23464  ptcmpfi  23778  ustfn  24167  ustn0  24186  retopbas  24725  blssioo  24760  xrtgioo  24772  zcld  24779  cnperf  24786  retopconn  24795  rembl  25507  mbfdm  25593  ismbf  25595  mbf0  25601  bddiblnc  25809  abelthlem9  26405  advlog  26618  advlogexp  26619  2irrexpq  26695  cxpcn3  26712  loglesqrt  26725  log2ub  26913  ppi1i  27131  cht2  27135  cht3  27136  bpos1lem  27245  lgslem4  27263  vmadivsum  27445  log2sumbnd  27507  selberg2  27514  selbergr  27531  nogt01o  27660  mulsproplem9  28116  1n0s  28340  n0fincut  28347  2nns  28410  istrkg2ld  28528  iscgrg  28580  ishpg  28827  ax5seglem7  29004  h2hva  31045  h2hsm  31046  h2hnm  31047  norm-ii-i  31208  hhshsslem2  31339  shincli  31433  chincli  31531  lnophdi  32073  imaelshi  32129  rnelshi  32130  bdophdi  32168  padct  32791  dfdec100  32903  dpadd2  32969  dpmul  32972  dpmul4  32973  nn0omnd  33404  nn0archi  33407  znfermltl  33426  ccfldextrr  33790  lmatfvlem  33959  rrhre  34165  sigaex  34254  br2base  34413  sxbrsigalem3  34416  carsgclctunlem3  34464  sitmcl  34495  rpsqrtcn  34737  hgt750lem  34795  hgt750lem2  34796  afsval  34815  kur14lem7  35394  retopsconn  35431  satfvsuclem1  35541  fmlasuc0  35566  hfuni  36366  neibastop2lem  36542  onint1  36631  ttcid  36674  bj-snfromadj  37351  topdifinffinlem  37663  poimirlem9  37950  poimirlem28  37969  poimirlem30  37971  poimirlem32  37973  ftc1cnnc  38013  cncfres  38086  lineset  40184  lautset  40528  pautsetN  40544  tendoset  41205  decpmulnc  42719  decpmul  42720  areaquad  43644  0fno  43862  finonex  43881  sblpnf  44737  lhe4.4ex1a  44756  fourierdlem62  46596  fourierdlem76  46610  lamberte  47336  65537prm  48039  11gbo  48251  bgoldbtbndlem1  48281  seppcld  49405  setc1onsubc  50077