Theorem eqeltrri 2825

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eltr3i  2840  zfrep4  5243  p0ex  5334  pp0ex  5336  ord3ex  5337  zfpair  5371  epse  5613  unexOLD  7701  fvresex  7918  opabex3  7925  abexssex  7928  abexex  7929  oprabrexex2  7936  seqomlem3  8397  1on  8423  2on  8424  inf0  9550  scottexs  9816  kardex  9823  infxpenlem  9942  r1om  10172  cfon  10184  fin23lem16  10264  fin1a2lem6  10334  hsmexlem5  10359  brdom7disj  10460  brdom6disj  10461  1lt2pi  10834  0cn  11142  resubcli  11460  0reALT  11495  1nn  12173  10nn  12641  numsucc  12665  nummac  12670  unirnioo  13386  ioorebas  13388  om2uzrani  13893  uzrdg0i  13900  hashunlei  14366  cats1fvn  14800  trclubi  14938  4sqlem19  16910  dec2dvds  17010  mod2xnegi  17018  modsubi  17019  gcdi  17020  isstruct2  17095  grppropstr  18867  nn0srg  21379  fermltlchr  21471  ltbval  21983  sn0topon  22918  indistop  22922  indisuni  22923  indistps2  22932  indistps2ALT  22934  restbas  23078  leordtval2  23132  iocpnfordt  23135  icomnfordt  23136  iooordt  23137  reordt  23138  dis1stc  23419  ptcmpfi  23733  ustfn  24122  ustn0  24141  retopbas  24681  blssioo  24716  xrtgioo  24728  zcld  24735  cnperf  24742  retopconn  24751  iimulcnOLD  24868  rembl  25474  mbfdm  25560  ismbf  25562  mbf0  25568  bddiblnc  25776  abelthlem9  26383  advlog  26596  advlogexp  26597  2irrexpq  26673  cxpcn3  26691  loglesqrt  26704  log2ub  26892  ppi1i  27111  cht2  27115  cht3  27116  bpos1lem  27226  lgslem4  27244  vmadivsum  27426  log2sumbnd  27488  selberg2  27495  selbergr  27512  nogt01o  27641  mulsproplem9  28067  1n0s  28280  n0sfincut  28286  2nns  28345  iscgrg  28492  ishpg  28739  ax5seglem7  28915  h2hva  30953  h2hsm  30954  h2hnm  30955  norm-ii-i  31116  hhshsslem2  31247  shincli  31341  chincli  31439  lnophdi  31981  imaelshi  32037  rnelshi  32038  bdophdi  32076  dfdec100  32805  dpadd2  32880  dpmul  32883  dpmul4  32884  nn0omnd  33309  nn0archi  33311  znfermltl  33330  ccfldextrr  33635  lmatfvlem  33798  rrhre  34004  sigaex  34093  br2base  34253  sxbrsigalem3  34256  carsgclctunlem3  34304  sitmcl  34335  rpsqrtcn  34577  hgt750lem  34635  hgt750lem2  34636  afsval  34655  kur14lem7  35192  retopsconn  35229  satfvsuclem1  35339  fmlasuc0  35364  hfuni  36165  neibastop2lem  36341  onint1  36430  bj-snfromadj  37025  topdifinffinlem  37328  poimirlem9  37616  poimirlem28  37635  poimirlem30  37637  poimirlem32  37639  ftc1cnnc  37679  cncfres  37752  lineset  39725  lautset  40069  pautsetN  40085  tendoset  40746  decpmulnc  42268  decpmul  42269  areaquad  43198  0no  43417  finonex  43436  sblpnf  44292  lhe4.4ex1a  44311  fourierdlem62  46159  fourierdlem76  46173  lamberte  46882  65537prm  47570  11gbo  47769  bgoldbtbndlem1  47799  seppcld  48911