Theorem eqeltrri 2832

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  3eltr3i  2847  zfrep4  5268  p0ex  5359  pp0ex  5361  ord3ex  5362  zfpair  5396  epse  5641  unexOLD  7744  fvresex  7963  opabex3  7971  abexssex  7974  abexex  7975  oprabrexex2  7982  seqomlem3  8471  1on  8497  2on  8499  inf0  9640  scottexs  9906  kardex  9913  infxpenlem  10032  r1om  10262  cfon  10274  fin23lem16  10354  fin1a2lem6  10424  hsmexlem5  10449  brdom7disj  10550  brdom6disj  10551  1lt2pi  10924  0cn  11232  resubcli  11550  0reALT  11585  1nn  12256  10nn  12729  numsucc  12753  nummac  12758  unirnioo  13471  ioorebas  13473  om2uzrani  13975  uzrdg0i  13982  hashunlei  14448  cats1fvn  14882  trclubi  15020  4sqlem19  16988  dec2dvds  17088  mod2xnegi  17096  modsubi  17097  gcdi  17098  isstruct2  17173  grppropstr  18941  nn0srg  21410  fermltlchr  21495  ltbval  22006  sn0topon  22941  indistop  22945  indisuni  22946  indistps2  22955  indistps2ALT  22957  restbas  23101  leordtval2  23155  iocpnfordt  23158  icomnfordt  23159  iooordt  23160  reordt  23161  dis1stc  23442  ptcmpfi  23756  ustfn  24145  ustn0  24164  retopbas  24704  blssioo  24739  xrtgioo  24751  zcld  24758  cnperf  24765  retopconn  24774  iimulcnOLD  24891  rembl  25498  mbfdm  25584  ismbf  25586  mbf0  25592  bddiblnc  25800  abelthlem9  26407  advlog  26620  advlogexp  26621  2irrexpq  26697  cxpcn3  26715  loglesqrt  26728  log2ub  26916  ppi1i  27135  cht2  27139  cht3  27140  bpos1lem  27250  lgslem4  27268  vmadivsum  27450  log2sumbnd  27512  selberg2  27519  selbergr  27536  nogt01o  27665  mulsproplem9  28084  1n0s  28297  n0sfincut  28303  2nns  28361  iscgrg  28496  ishpg  28743  ax5seglem7  28919  h2hva  30960  h2hsm  30961  h2hnm  30962  norm-ii-i  31123  hhshsslem2  31254  shincli  31348  chincli  31446  lnophdi  31988  imaelshi  32044  rnelshi  32045  bdophdi  32083  dfdec100  32814  dpadd2  32889  dpmul  32892  dpmul4  32893  nn0omnd  33365  nn0archi  33367  znfermltl  33386  ccfldextrr  33693  lmatfvlem  33851  rrhre  34057  sigaex  34146  br2base  34306  sxbrsigalem3  34309  carsgclctunlem3  34357  sitmcl  34388  rpsqrtcn  34630  hgt750lem  34688  hgt750lem2  34689  afsval  34708  kur14lem7  35239  retopsconn  35276  satfvsuclem1  35386  fmlasuc0  35411  hfuni  36207  neibastop2lem  36383  onint1  36472  bj-snfromadj  37067  topdifinffinlem  37370  poimirlem9  37658  poimirlem28  37677  poimirlem30  37679  poimirlem32  37681  ftc1cnnc  37721  cncfres  37794  lineset  39762  lautset  40106  pautsetN  40122  tendoset  40783  decpmulnc  42305  decpmul  42306  areaquad  43215  0no  43434  finonex  43453  sblpnf  44309  lhe4.4ex1a  44328  fourierdlem62  46177  fourierdlem76  46191  lamberte  46900  65537prm  47570  11gbo  47769  bgoldbtbndlem1  47799  seppcld  48884