Theorem eqeltrri 2828

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

Syntax hints:   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  3eltr3i  2843  zfrep4  5229  p0ex  5320  pp0ex  5322  ord3ex  5323  zfpair  5357  epse  5596  unexOLD  7678  fvresex  7892  opabex3  7899  abexssex  7902  abexex  7903  oprabrexex2  7910  seqomlem3  8371  1on  8397  2on  8398  inf0  9511  scottexs  9780  kardex  9787  infxpenlem  9904  r1om  10134  cfon  10146  fin23lem16  10226  fin1a2lem6  10296  hsmexlem5  10321  brdom7disj  10422  brdom6disj  10423  1lt2pi  10796  0cn  11104  resubcli  11423  0reALT  11458  1nn  12136  10nn  12604  numsucc  12628  nummac  12633  unirnioo  13349  ioorebas  13351  om2uzrani  13859  uzrdg0i  13866  hashunlei  14332  cats1fvn  14765  trclubi  14903  4sqlem19  16875  dec2dvds  16975  mod2xnegi  16983  modsubi  16984  gcdi  16985  isstruct2  17060  grppropstr  18866  nn0srg  21374  fermltlchr  21466  ltbval  21978  sn0topon  22913  indistop  22917  indisuni  22918  indistps2  22927  indistps2ALT  22929  restbas  23073  leordtval2  23127  iocpnfordt  23130  icomnfordt  23131  iooordt  23132  reordt  23133  dis1stc  23414  ptcmpfi  23728  ustfn  24117  ustn0  24136  retopbas  24675  blssioo  24710  xrtgioo  24722  zcld  24729  cnperf  24736  retopconn  24745  iimulcnOLD  24862  rembl  25468  mbfdm  25554  ismbf  25556  mbf0  25562  bddiblnc  25770  abelthlem9  26377  advlog  26590  advlogexp  26591  2irrexpq  26667  cxpcn3  26685  loglesqrt  26698  log2ub  26886  ppi1i  27105  cht2  27109  cht3  27110  bpos1lem  27220  lgslem4  27238  vmadivsum  27420  log2sumbnd  27482  selberg2  27489  selbergr  27506  nogt01o  27635  mulsproplem9  28063  1n0s  28276  n0sfincut  28282  2nns  28341  iscgrg  28490  ishpg  28737  ax5seglem7  28913  h2hva  30954  h2hsm  30955  h2hnm  30956  norm-ii-i  31117  hhshsslem2  31248  shincli  31342  chincli  31440  lnophdi  31982  imaelshi  32038  rnelshi  32039  bdophdi  32077  dfdec100  32813  dpadd2  32890  dpmul  32893  dpmul4  32894  nn0omnd  33309  nn0archi  33312  znfermltl  33331  ccfldextrr  33659  lmatfvlem  33828  rrhre  34034  sigaex  34123  br2base  34282  sxbrsigalem3  34285  carsgclctunlem3  34333  sitmcl  34364  rpsqrtcn  34606  hgt750lem  34664  hgt750lem2  34665  afsval  34684  kur14lem7  35256  retopsconn  35293  satfvsuclem1  35403  fmlasuc0  35428  hfuni  36228  neibastop2lem  36404  onint1  36493  bj-snfromadj  37088  topdifinffinlem  37391  poimirlem9  37668  poimirlem28  37687  poimirlem30  37689  poimirlem32  37691  ftc1cnnc  37731  cncfres  37804  lineset  39836  lautset  40180  pautsetN  40196  tendoset  40857  decpmulnc  42379  decpmul  42380  areaquad  43308  0no  43527  finonex  43546  sblpnf  44402  lhe4.4ex1a  44421  fourierdlem62  46265  fourierdlem76  46279  lamberte  46987  65537prm  47675  11gbo  47874  bgoldbtbndlem1  47904  seppcld  49029