Theorem eqeltrri 2685

Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqeltrr.1	⊢ 𝐴 = 𝐵
eqeltrr.2	⊢ 𝐴 ∈ 𝐶

Assertion

Ref	Expression
eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2619	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrr.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2684	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  3eltr3i  2700  zfrep4  4707  p0ex  4779  pp0ex  4781  ord3ex  4782  zfpair  4831  epse  5021  unex  6854  fvresex  7032  abrexex  7033  opabex3  7038  abrexex2  7040  abexssex  7041  abexex  7042  oprabrexex2  7049  seqomlem3  7434  inf0  8401  scottexs  8633  kardex  8640  infxpenlem  8719  r1om  8949  cfon  8960  fin23lem16  9040  fin1a2lem6  9110  hsmexlem5  9135  brdom7disj  9234  brdom6disj  9235  1lt2pi  9606  0cn  9911  resubcli  10222  0reALT  10257  1nn  10908  10nn  11390  numsucc  11425  nummac  11434  unirnioo  12144  ioorebas  12146  fz0to4untppr  12311  om2uzrani  12613  uzrdg0i  12620  hashunlei  13072  cats1fvn  13454  trclubi  13583  trclubiOLD  13584  4sqlem19  15505  dec2dvds  15605  mod2xnegi  15613  modsubi  15614  gcdi  15615  isstruct2  15704  grppropstr  17262  ltbval  19292  nn0srg  19635  sn0topon  20612  indistop  20616  indisuni  20617  indistps2  20626  indistps2ALT  20628  restbas  20772  leordtval2  20826  iocpnfordt  20829  icomnfordt  20830  iooordt  20831  reordt  20832  dis1stc  21112  ptcmpfi  21426  ustfn  21815  ustn0  21834  retopbas  22374  blssioo  22406  xrtgioo  22417  zcld  22424  cnperf  22431  retopcon  22440  iimulcn  22545  rembl  23115  mbfdm  23201  ismbf  23203  abelthlem9  23998  advlog  24200  advlogexp  24201  cxpcn3  24289  loglesqrt  24299  log2ub  24476  ppi1i  24694  cht2  24698  cht3  24699  bpos1lem  24807  lgslem4  24825  vmadivsum  24971  log2sumbnd  25033  selberg2  25040  selbergr  25057  iscgrg  25207  ishpg  25451  ax5seglem7  25615  iseupa  26492  h2hva  27215  h2hsm  27216  h2hnm  27217  norm-ii-i  27378  hhshsslem2  27509  shincli  27605  chincli  27703  lnophdi  28245  imaelshi  28301  rnelshi  28302  bdophdi  28340  nn0omnd  29172  nn0archi  29174  lmatfvlem  29209  rmulccn  29302  rrhre  29393  sigaex  29499  br2base  29658  sxbrsigalem3  29661  carsgclctunlem3  29709  sitmcl  29740  afsval  30002  kur14lem7  30448  retopscon  30485  hfuni  31461  neibastop2lem  31525  onint1  31618  topdifinffinlem  32371  poimirlem9  32588  poimirlem28  32607  poimirlem30  32609  poimirlem32  32611  0mbf  32625  bddiblnc  32650  ftc1cnnc  32654  cncfres  32734  lineset  34042  lautset  34386  pautsetN  34402  tendoset  35065  areaquad  36821  sblpnf  37531  lhe4.4ex1a  37550  fourierdlem62  39061  fourierdlem76  39075  65537prm  40026  11gboa  40197  bgoldbtbndlem1  40221  fusgrfis  40549