Theorem eqeltrri 2908

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

Syntax hints:   = wceq 1530   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-clel 2891

This theorem is referenced by:  3eltr3i  2923  zfrep4  5191  p0ex  5275  pp0ex  5277  ord3ex  5278  zfpair  5312  epse  5531  unex  7461  fvresex  7653  opabex3  7660  abexssex  7663  abexex  7664  oprabrexex2  7671  seqomlem3  8080  inf0  9076  scottexs  9308  kardex  9315  infxpenlem  9431  r1om  9658  cfon  9669  fin23lem16  9749  fin1a2lem6  9819  hsmexlem5  9844  brdom7disj  9945  brdom6disj  9946  1lt2pi  10319  0cn  10625  resubcli  10940  0reALT  10975  1nn  11641  10nn  12106  numsucc  12130  nummac  12135  unirnioo  12829  ioorebas  12831  fz0to4untppr  13002  om2uzrani  13312  uzrdg0i  13319  hashunlei  13778  cats1fvn  14212  trclubi  14348  4sqlem19  16291  dec2dvds  16391  mod2xnegi  16399  modsubi  16400  gcdi  16401  isstruct2  16485  grppropstr  18112  ltbval  20244  nn0srg  20607  sn0topon  21598  indistop  21602  indisuni  21603  indistps2  21612  indistps2ALT  21614  restbas  21758  leordtval2  21812  iocpnfordt  21815  icomnfordt  21816  iooordt  21817  reordt  21818  dis1stc  22099  ptcmpfi  22413  ustfn  22802  ustn0  22821  retopbas  23361  blssioo  23395  xrtgioo  23406  zcld  23413  cnperf  23420  retopconn  23429  iimulcn  23534  rembl  24133  mbfdm  24219  ismbf  24221  mbf0  24227  abelthlem9  25020  advlog  25229  advlogexp  25230  2irrexpq  25305  cxpcn3  25321  loglesqrt  25331  log2ub  25519  ppi1i  25737  cht2  25741  cht3  25742  bpos1lem  25850  lgslem4  25868  vmadivsum  26050  log2sumbnd  26112  selberg2  26119  selbergr  26136  iscgrg  26290  ishpg  26537  ax5seglem7  26713  h2hva  28743  h2hsm  28744  h2hnm  28745  norm-ii-i  28906  hhshsslem2  29037  shincli  29131  chincli  29229  lnophdi  29771  imaelshi  29827  rnelshi  29828  bdophdi  29866  dfdec100  30539  dpadd2  30579  dpmul  30582  dpmul4  30583  nn0omnd  30907  nn0archi  30909  ccfldextrr  31031  lmatfvlem  31073  rmulccn  31164  rrhre  31255  sigaex  31362  br2base  31520  sxbrsigalem3  31523  carsgclctunlem3  31571  sitmcl  31602  rpsqrtcn  31857  hgt750lem  31915  hgt750lem2  31916  afsval  31935  kur14lem7  32452  retopsconn  32489  satfvsuclem1  32599  fmlasuc0  32624  hfuni  33638  neibastop2lem  33701  onint1  33790  topdifinffinlem  34620  poimirlem9  34893  poimirlem28  34912  poimirlem30  34914  poimirlem32  34916  bddiblnc  34954  ftc1cnnc  34958  cncfres  35035  lineset  36866  lautset  37210  pautsetN  37226  tendoset  37887  decpmulnc  39163  decpmul  39164  areaquad  39813  sblpnf  40632  lhe4.4ex1a  40651  fourierdlem62  42443  fourierdlem76  42457  65537prm  43728  11gbo  43930  bgoldbtbndlem1  43960