Theorem eqeltrri 2838

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

Syntax hints:   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  3eltr3i  2853  zfrep4  5293  p0ex  5384  pp0ex  5386  ord3ex  5387  zfpair  5421  epse  5667  unexOLD  7765  fvresex  7984  opabex3  7992  abexssex  7995  abexex  7996  oprabrexex2  8003  seqomlem3  8492  1on  8518  2on  8520  inf0  9661  scottexs  9927  kardex  9934  infxpenlem  10053  r1om  10283  cfon  10295  fin23lem16  10375  fin1a2lem6  10445  hsmexlem5  10470  brdom7disj  10571  brdom6disj  10572  1lt2pi  10945  0cn  11253  resubcli  11571  0reALT  11606  1nn  12277  10nn  12749  numsucc  12773  nummac  12778  unirnioo  13489  ioorebas  13491  om2uzrani  13993  uzrdg0i  14000  hashunlei  14464  cats1fvn  14897  trclubi  15035  4sqlem19  17001  dec2dvds  17101  mod2xnegi  17109  modsubi  17110  gcdi  17111  isstruct2  17186  grppropstr  18971  nn0srg  21455  fermltlchr  21544  ltbval  22061  sn0topon  23005  indistop  23009  indisuni  23010  indistps2  23019  indistps2ALT  23022  restbas  23166  leordtval2  23220  iocpnfordt  23223  icomnfordt  23224  iooordt  23225  reordt  23226  dis1stc  23507  ptcmpfi  23821  ustfn  24210  ustn0  24229  retopbas  24781  blssioo  24816  xrtgioo  24828  zcld  24835  cnperf  24842  retopconn  24851  iimulcnOLD  24968  rembl  25575  mbfdm  25661  ismbf  25663  mbf0  25669  bddiblnc  25877  abelthlem9  26484  advlog  26696  advlogexp  26697  2irrexpq  26773  cxpcn3  26791  loglesqrt  26804  log2ub  26992  ppi1i  27211  cht2  27215  cht3  27216  bpos1lem  27326  lgslem4  27344  vmadivsum  27526  log2sumbnd  27588  selberg2  27595  selbergr  27612  nogt01o  27741  mulsproplem9  28150  1n0s  28351  2nns  28402  iscgrg  28520  ishpg  28767  ax5seglem7  28950  h2hva  30993  h2hsm  30994  h2hnm  30995  norm-ii-i  31156  hhshsslem2  31287  shincli  31381  chincli  31479  lnophdi  32021  imaelshi  32077  rnelshi  32078  bdophdi  32116  dfdec100  32832  dpadd2  32892  dpmul  32895  dpmul4  32896  nn0omnd  33373  nn0archi  33375  znfermltl  33394  ccfldextrr  33699  lmatfvlem  33814  rrhre  34022  sigaex  34111  br2base  34271  sxbrsigalem3  34274  carsgclctunlem3  34322  sitmcl  34353  rpsqrtcn  34608  hgt750lem  34666  hgt750lem2  34667  afsval  34686  kur14lem7  35217  retopsconn  35254  satfvsuclem1  35364  fmlasuc0  35389  hfuni  36185  neibastop2lem  36361  onint1  36450  bj-snfromadj  37045  topdifinffinlem  37348  poimirlem9  37636  poimirlem28  37655  poimirlem30  37657  poimirlem32  37659  ftc1cnnc  37699  cncfres  37772  lineset  39740  lautset  40084  pautsetN  40100  tendoset  40761  decpmulnc  42322  decpmul  42323  areaquad  43228  0no  43448  finonex  43467  sblpnf  44329  lhe4.4ex1a  44348  fourierdlem62  46183  fourierdlem76  46197  65537prm  47563  11gbo  47762  bgoldbtbndlem1  47792  seppcld  48827