Theorem eqeltrri 2836

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

Syntax hints:   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  3eltr3i  2851  zfrep4  5215  p0ex  5302  pp0ex  5304  ord3ex  5305  zfpair  5339  epse  5563  unex  7574  fvresex  7776  opabex3  7783  abexssex  7786  abexex  7787  oprabrexex2  7794  seqomlem3  8253  inf0  9309  scottexs  9576  kardex  9583  infxpenlem  9700  r1om  9931  cfon  9942  fin23lem16  10022  fin1a2lem6  10092  hsmexlem5  10117  brdom7disj  10218  brdom6disj  10219  1lt2pi  10592  0cn  10898  resubcli  11213  0reALT  11248  1nn  11914  10nn  12382  numsucc  12406  nummac  12411  unirnioo  13110  ioorebas  13112  fz0to4untppr  13288  om2uzrani  13600  uzrdg0i  13607  hashunlei  14068  cats1fvn  14499  trclubi  14635  4sqlem19  16592  dec2dvds  16692  mod2xnegi  16700  modsubi  16701  gcdi  16702  isstruct2  16778  grppropstr  18511  nn0srg  20580  ltbval  21154  sn0topon  22056  indistop  22060  indisuni  22061  indistps2  22070  indistps2ALT  22073  restbas  22217  leordtval2  22271  iocpnfordt  22274  icomnfordt  22275  iooordt  22276  reordt  22277  dis1stc  22558  ptcmpfi  22872  ustfn  23261  ustn0  23280  retopbas  23830  blssioo  23864  xrtgioo  23875  zcld  23882  cnperf  23889  retopconn  23898  iimulcn  24007  rembl  24609  mbfdm  24695  ismbf  24697  mbf0  24703  bddiblnc  24911  abelthlem9  25504  advlog  25714  advlogexp  25715  2irrexpq  25790  cxpcn3  25806  loglesqrt  25816  log2ub  26004  ppi1i  26222  cht2  26226  cht3  26227  bpos1lem  26335  lgslem4  26353  vmadivsum  26535  log2sumbnd  26597  selberg2  26604  selbergr  26621  iscgrg  26777  ishpg  27024  ax5seglem7  27206  h2hva  29237  h2hsm  29238  h2hnm  29239  norm-ii-i  29400  hhshsslem2  29531  shincli  29625  chincli  29723  lnophdi  30265  imaelshi  30321  rnelshi  30322  bdophdi  30360  dfdec100  31046  dpadd2  31086  dpmul  31089  dpmul4  31090  nn0omnd  31447  nn0archi  31449  znfermltl  31464  ccfldextrr  31625  lmatfvlem  31667  rmulccn  31780  rrhre  31871  sigaex  31978  br2base  32136  sxbrsigalem3  32139  carsgclctunlem3  32187  sitmcl  32218  rpsqrtcn  32473  hgt750lem  32531  hgt750lem2  32532  afsval  32551  kur14lem7  33074  retopsconn  33111  satfvsuclem1  33221  fmlasuc0  33246  nogt01o  33826  hfuni  34413  neibastop2lem  34476  onint1  34565  topdifinffinlem  35445  poimirlem9  35713  poimirlem28  35732  poimirlem30  35734  poimirlem32  35736  ftc1cnnc  35776  cncfres  35850  lineset  37679  lautset  38023  pautsetN  38039  tendoset  38700  decpmulnc  40236  decpmul  40237  areaquad  40963  sblpnf  41817  lhe4.4ex1a  41836  fourierdlem62  43599  fourierdlem76  43613  65537prm  44916  11gbo  45115  bgoldbtbndlem1  45145  seppcld  46111