Theorem eqeltrri 2857

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 2769	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2856	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 2732

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

This theorem is used by:  3eltr3i  2872  zfrep4  5246  p0ex  5346  pp0ex  5348  ord3ex  5349  zfpair  5383  moabex  5426  epse  5630  fvresex  7956  opabex3  7963  abexssex  7966  abexex  7967  oprabrexex2  7974  seqomlem3  8441  1on  8468  2on  8469  inf0  9600  hfuni  9883  scottexsOLD  9900  kardexOLD  9915  infxpenlem  10049  r1om  10278  cfonOLD  10290  fin23lem16  10370  fin1a2lem6  10440  hsmexlem5  10465  brdom7disj  10567  brdom6disj  10568  1lt2pi  10947  0cn  11255  resubcli  11577  0reALT  11612  1nn  12301  10nn  12789  numsucc  12814  nummac  12819  unirnioo  13535  ioorebas  13537  om2uzrani  14049  uzrdg0i  14056  hashunlei  14523  cats1fvn  14962  trclubi  15102  sgnrn  15204  4sqlem19  17088  dec2dvds  17188  mod2xnegi  17196  modsubi  17197  gcdi  17198  isstruct2  17274  smndex1gbas  19045  smndex1gid  19047  smndex1igid  19049  grppropstr  19111  nn0srg  21690  fermltlchr  21782  ltbval  22299  sn0topon  23263  indistop  23267  indisuni  23268  indistps2  23277  indistps2ALT  23279  restbas  23423  leordtval2  23477  iocpnfordt  23480  icomnfordt  23481  iooordt  23482  reordt  23483  dis1stc  23765  ptcmpfi  24079  ustfn  24468  ustn0  24487  retopbas  25026  blssioo  25061  xrtgioo  25073  zcld  25080  cnperf  25087  retopconn  25096  rembl  25808  mbfdm  25894  ismbf  25896  mbf0  25902  bddiblnc  26109  abelthlem9  26716  advlog  26931  advlogexp  26932  2irrexpq  27008  cxpcn3  27025  loglesqrt  27038  log2ub  27226  ppi1i  27444  cht2  27448  cht3  27449  bpos1lem  27558  lgslem4  27576  vmadivsum  27758  log2sumbnd  27820  selberg2  27827  selbergr  27844  nogt01o  27972  mulsproplem9  28429  1n0s  28653  n0fincut  28660  2nns  28723  istrkg2ld  28841  iscgrg  28894  ishpg  29156  ax5seglem7  29432  h2hva  31495  h2hsm  31496  h2hnm  31497  norm-ii-i  31658  hhshsslem2  31789  shincli  31883  chincli  31981  lnophdi  32523  imaelshi  32579  rnelshi  32580  bdophdi  32618  padct  33229  dfdec100  33340  dpadd2  33395  dpmul  33398  dpmul4  33399  nn0omnd  33824  nn0archi  33827  znfermltl  33841  ccfldextrr  34197  lmatfvlem  34366  rrhre  34572  sigaex  34661  br2base  34821  sxbrsigalem3  34824  carsgclctunlem3  34872  sitmcl  34903  rpsqrtcn  35142  hgt750lem  35200  hgt750lem2  35201  afsval  35223  kur14lem7  35892  retopsconn  35929  satfvsuclem1  36039  fmlasuc0  36064  neibastop2lem  37064  onint1  37153  ttcid  37196  bj-snfromadj  37873  topdifinffinlem  38184  poimirlem9  38461  poimirlem28  38480  poimirlem30  38482  poimirlem32  38484  ftc1cnnc  38524  dfproplem  38555  cncfres  38613  scottexf  39014  lineset  40709  lautset  41053  pautsetN  41069  tendoset  41730  decpmulnc  43260  decpmul  43261  areaquad  44155  0fno  44373  finonex  44392  sblpnf  45232  lhe4.4ex1a  45251  fourierdlem62  47094  fourierdlem76  47108  lamberte  47854  65537prm  48577  11gbo  48789  bgoldbtbndlem1  48819  seppcld  49954  setc1onsubc  50626