Theorem eqeltrri 2866

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

Syntax hints:   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  3eltr3i  2881  zfrep4  5258  p0ex  5358  pp0ex  5360  ord3ex  5361  zfpair  5395  moabex  5442  epse  5646  unexOLD  7746  fvresex  7959  opabex3  7966  abexssex  7969  abexex  7970  oprabrexex2  7977  seqomlem3  8441  1on  8468  2on  8469  inf0  9592  scottexs  9863  kardex  9882  infxpenlem  9999  r1om  10228  cfonOLD  10241  fin23lem16  10321  fin1a2lem6  10391  hsmexlem5  10416  brdom7disj  10517  brdom6disj  10518  1lt2pi  10892  0cn  11200  resubcli  11522  0reALT  11557  1nn  12246  10nn  12733  numsucc  12758  nummac  12763  unirnioo  13478  ioorebas  13480  om2uzrani  13990  uzrdg0i  13997  hashunlei  14464  cats1fvn  14897  trclubi  15035  sgnrn  15137  4sqlem19  17025  dec2dvds  17125  mod2xnegi  17133  modsubi  17134  gcdi  17135  isstruct2  17211  smndex1gbas  18963  smndex1gid  18965  smndex1igid  18967  grppropstr  19022  nn0srg  21558  fermltlchr  21650  ltbval  22165  sn0topon  23126  indistop  23130  indisuni  23131  indistps2  23140  indistps2ALT  23142  restbas  23286  leordtval2  23340  iocpnfordt  23343  icomnfordt  23344  iooordt  23345  reordt  23346  dis1stc  23627  ptcmpfi  23941  ustfn  24330  ustn0  24349  retopbas  24888  blssioo  24923  xrtgioo  24935  zcld  24942  cnperf  24949  retopconn  24958  rembl  25670  mbfdm  25756  ismbf  25758  mbf0  25764  bddiblnc  25972  abelthlem9  26571  advlog  26787  advlogexp  26788  2irrexpq  26864  cxpcn3  26881  loglesqrt  26894  log2ub  27082  ppi1i  27300  cht2  27304  cht3  27305  bpos1lem  27414  lgslem4  27432  vmadivsum  27614  log2sumbnd  27676  selberg2  27683  selbergr  27700  nogt01o  27828  mulsproplem9  28285  1n0s  28509  n0fincut  28516  2nns  28579  istrkg2ld  28697  iscgrg  28749  ishpg  29002  ax5seglem7  29228  h2hva  31269  h2hsm  31270  h2hnm  31271  norm-ii-i  31432  hhshsslem2  31563  shincli  31657  chincli  31755  lnophdi  32297  imaelshi  32353  rnelshi  32354  bdophdi  32392  padct  33006  dfdec100  33117  dpadd2  33172  dpmul  33175  dpmul4  33176  nn0omnd  33609  nn0archi  33612  znfermltl  33626  ccfldextrr  33983  lmatfvlem  34152  rrhre  34358  sigaex  34447  br2base  34606  sxbrsigalem3  34609  carsgclctunlem3  34657  sitmcl  34688  rpsqrtcn  34927  hgt750lem  34985  hgt750lem2  34986  afsval  35008  kur14lem7  35639  retopsconn  35676  satfvsuclem1  35786  fmlasuc0  35811  hfuni  36611  neibastop2lem  36796  onint1  36885  ttcid  36928  bj-snfromadj  37605  topdifinffinlem  37918  poimirlem9  38205  poimirlem28  38224  poimirlem30  38226  poimirlem32  38228  ftc1cnnc  38268  cncfres  38341  lineset  40439  lautset  40783  pautsetN  40799  tendoset  41460  decpmulnc  42975  decpmul  42976  areaquad  43872  0fno  44090  finonex  44109  sblpnf  44949  lhe4.4ex1a  44968  fourierdlem62  46811  fourierdlem76  46825  lamberte  47551  65537prm  48254  11gbo  48466  bgoldbtbndlem1  48496  seppcld  49630  setc1onsubc  50302