Theorem eqeltrri 2859

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837

This theorem is used by:  3eltr3i  2874  zfrep4  5252  p0ex  5353  pp0ex  5355  ord3ex  5356  zfpair  5390  moabex  5437  epse  5641  fvresex  7960  opabex3  7967  abexssex  7970  abexex  7971  oprabrexex2  7978  seqomlem3  8444  1on  8471  2on  8472  inf0  9603  scottexsOLD  9885  kardexOLD  9900  infxpenlem  10019  r1om  10248  cfonOLD  10260  fin23lem16  10340  fin1a2lem6  10410  hsmexlem5  10435  brdom7disj  10537  brdom6disj  10538  1lt2pi  10915  0cn  11223  resubcli  11545  0reALT  11580  1nn  12269  10nn  12757  numsucc  12782  nummac  12787  unirnioo  13502  ioorebas  13504  om2uzrani  14016  uzrdg0i  14023  hashunlei  14490  cats1fvn  14929  trclubi  15069  sgnrn  15171  4sqlem19  17057  dec2dvds  17157  mod2xnegi  17165  modsubi  17166  gcdi  17167  isstruct2  17243  smndex1gbas  19010  smndex1gid  19012  smndex1igid  19014  grppropstr  19076  nn0srg  21649  fermltlchr  21741  ltbval  22258  sn0topon  23222  indistop  23226  indisuni  23227  indistps2  23236  indistps2ALT  23238  restbas  23382  leordtval2  23436  iocpnfordt  23439  icomnfordt  23440  iooordt  23441  reordt  23442  dis1stc  23724  ptcmpfi  24038  ustfn  24427  ustn0  24446  retopbas  24985  blssioo  25020  xrtgioo  25032  zcld  25039  cnperf  25046  retopconn  25055  rembl  25767  mbfdm  25853  ismbf  25855  mbf0  25861  bddiblnc  26069  abelthlem9  26671  advlog  26887  advlogexp  26888  2irrexpq  26964  cxpcn3  26981  loglesqrt  26994  log2ub  27182  ppi1i  27400  cht2  27404  cht3  27405  bpos1lem  27514  lgslem4  27532  vmadivsum  27714  log2sumbnd  27776  selberg2  27783  selbergr  27800  nogt01o  27928  mulsproplem9  28385  1n0s  28609  n0fincut  28616  2nns  28679  istrkg2ld  28797  iscgrg  28850  ishpg  29112  ax5seglem7  29376  h2hva  31439  h2hsm  31440  h2hnm  31441  norm-ii-i  31602  hhshsslem2  31733  shincli  31827  chincli  31925  lnophdi  32467  imaelshi  32523  rnelshi  32524  bdophdi  32562  padct  33174  dfdec100  33285  dpadd2  33340  dpmul  33343  dpmul4  33344  nn0omnd  33769  nn0archi  33772  znfermltl  33786  ccfldextrr  34141  lmatfvlem  34310  rrhre  34516  sigaex  34605  br2base  34765  sxbrsigalem3  34768  carsgclctunlem3  34816  sitmcl  34847  rpsqrtcn  35086  hgt750lem  35144  hgt750lem2  35145  afsval  35167  kur14lem7  35776  retopsconn  35813  satfvsuclem1  35923  fmlasuc0  35948  hfuni  36749  neibastop2lem  36964  onint1  37053  ttcid  37096  bj-snfromadj  37773  topdifinffinlem  38086  poimirlem9  38363  poimirlem28  38382  poimirlem30  38384  poimirlem32  38386  ftc1cnnc  38426  cncfres  38500  scottexf  38901  lineset  40596  lautset  40940  pautsetN  40956  tendoset  41617  decpmulnc  43147  decpmul  43148  areaquad  44042  0fno  44260  finonex  44279  sblpnf  45119  lhe4.4ex1a  45138  fourierdlem62  46981  fourierdlem76  46995  lamberte  47741  65537prm  48464  11gbo  48676  bgoldbtbndlem1  48706  seppcld  49841  setc1onsubc  50513