Theorem eqeltrri 2841

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

Syntax hints:   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  3eltr3i  2856  zfrep4  5314  p0ex  5402  pp0ex  5404  ord3ex  5405  zfpair  5439  epse  5682  unexOLD  7780  fvresex  8000  opabex3  8008  abexssex  8011  abexex  8012  oprabrexex2  8019  seqomlem3  8508  1on  8534  2on  8536  inf0  9690  scottexs  9956  kardex  9963  infxpenlem  10082  r1om  10312  cfon  10324  fin23lem16  10404  fin1a2lem6  10474  hsmexlem5  10499  brdom7disj  10600  brdom6disj  10601  1lt2pi  10974  0cn  11282  resubcli  11598  0reALT  11633  1nn  12304  10nn  12774  numsucc  12798  nummac  12803  unirnioo  13509  ioorebas  13511  om2uzrani  14003  uzrdg0i  14010  hashunlei  14474  cats1fvn  14907  trclubi  15045  4sqlem19  17010  dec2dvds  17110  mod2xnegi  17118  modsubi  17119  gcdi  17120  isstruct2  17196  grppropstr  18993  nn0srg  21478  fermltlchr  21567  ltbval  22084  sn0topon  23026  indistop  23030  indisuni  23031  indistps2  23040  indistps2ALT  23043  restbas  23187  leordtval2  23241  iocpnfordt  23244  icomnfordt  23245  iooordt  23246  reordt  23247  dis1stc  23528  ptcmpfi  23842  ustfn  24231  ustn0  24250  retopbas  24802  blssioo  24836  xrtgioo  24847  zcld  24854  cnperf  24861  retopconn  24870  iimulcnOLD  24987  rembl  25594  mbfdm  25680  ismbf  25682  mbf0  25688  bddiblnc  25897  abelthlem9  26502  advlog  26714  advlogexp  26715  2irrexpq  26791  cxpcn3  26809  loglesqrt  26822  log2ub  27010  ppi1i  27229  cht2  27233  cht3  27234  bpos1lem  27344  lgslem4  27362  vmadivsum  27544  log2sumbnd  27606  selberg2  27613  selbergr  27630  nogt01o  27759  mulsproplem9  28168  1n0s  28369  2nns  28420  iscgrg  28538  ishpg  28785  ax5seglem7  28968  h2hva  31006  h2hsm  31007  h2hnm  31008  norm-ii-i  31169  hhshsslem2  31300  shincli  31394  chincli  31492  lnophdi  32034  imaelshi  32090  rnelshi  32091  bdophdi  32129  dfdec100  32834  dpadd2  32874  dpmul  32877  dpmul4  32878  nn0omnd  33338  nn0archi  33340  znfermltl  33359  ccfldextrr  33661  lmatfvlem  33761  rrhre  33967  sigaex  34074  br2base  34234  sxbrsigalem3  34237  carsgclctunlem3  34285  sitmcl  34316  rpsqrtcn  34570  hgt750lem  34628  hgt750lem2  34629  afsval  34648  kur14lem7  35180  retopsconn  35217  satfvsuclem1  35327  fmlasuc0  35352  hfuni  36148  neibastop2lem  36326  onint1  36415  bj-snfromadj  37010  topdifinffinlem  37313  poimirlem9  37589  poimirlem28  37608  poimirlem30  37610  poimirlem32  37612  ftc1cnnc  37652  cncfres  37725  lineset  39695  lautset  40039  pautsetN  40055  tendoset  40716  decpmulnc  42276  decpmul  42277  areaquad  43177  0no  43397  finonex  43416  sblpnf  44279  lhe4.4ex1a  44298  fourierdlem62  46089  fourierdlem76  46103  65537prm  47450  11gbo  47649  bgoldbtbndlem1  47679  seppcld  48609