Theorem eqeltrri 2834

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 2833	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  3eltr3i  2849  zfrep4  5239  p0ex  5330  pp0ex  5332  ord3ex  5333  zfpair  5367  moabex  5407  epse  5607  unexOLD  7692  fvresex  7906  opabex3  7913  abexssex  7916  abexex  7917  oprabrexex2  7924  seqomlem3  8385  1on  8411  2on  8412  inf0  9534  scottexs  9803  kardex  9810  infxpenlem  9927  r1om  10157  cfon  10169  fin23lem16  10249  fin1a2lem6  10319  hsmexlem5  10344  brdom7disj  10445  brdom6disj  10446  1lt2pi  10820  0cn  11128  resubcli  11447  0reALT  11482  1nn  12160  10nn  12627  numsucc  12651  nummac  12656  unirnioo  13369  ioorebas  13371  om2uzrani  13879  uzrdg0i  13886  hashunlei  14352  cats1fvn  14785  trclubi  14923  4sqlem19  16895  dec2dvds  16995  mod2xnegi  17003  modsubi  17004  gcdi  17005  isstruct2  17080  grppropstr  18887  nn0srg  21396  fermltlchr  21488  ltbval  22002  sn0topon  22946  indistop  22950  indisuni  22951  indistps2  22960  indistps2ALT  22962  restbas  23106  leordtval2  23160  iocpnfordt  23163  icomnfordt  23164  iooordt  23165  reordt  23166  dis1stc  23447  ptcmpfi  23761  ustfn  24150  ustn0  24169  retopbas  24708  blssioo  24743  xrtgioo  24755  zcld  24762  cnperf  24769  retopconn  24778  iimulcnOLD  24895  rembl  25501  mbfdm  25587  ismbf  25589  mbf0  25595  bddiblnc  25803  abelthlem9  26410  advlog  26623  advlogexp  26624  2irrexpq  26700  cxpcn3  26718  loglesqrt  26731  log2ub  26919  ppi1i  27138  cht2  27142  cht3  27143  bpos1lem  27253  lgslem4  27271  vmadivsum  27453  log2sumbnd  27515  selberg2  27522  selbergr  27539  nogt01o  27668  mulsproplem9  28124  1n0s  28348  n0fincut  28355  2nns  28418  iscgrg  28588  ishpg  28835  ax5seglem7  29012  h2hva  31053  h2hsm  31054  h2hnm  31055  norm-ii-i  31216  hhshsslem2  31347  shincli  31441  chincli  31539  lnophdi  32081  imaelshi  32137  rnelshi  32138  bdophdi  32176  dfdec100  32913  dpadd2  32993  dpmul  32996  dpmul4  32997  nn0omnd  33427  nn0archi  33430  znfermltl  33449  ccfldextrr  33805  lmatfvlem  33974  rrhre  34180  sigaex  34269  br2base  34428  sxbrsigalem3  34431  carsgclctunlem3  34479  sitmcl  34510  rpsqrtcn  34752  hgt750lem  34810  hgt750lem2  34811  afsval  34830  kur14lem7  35408  retopsconn  35445  satfvsuclem1  35555  fmlasuc0  35580  hfuni  36380  neibastop2lem  36556  onint1  36645  bj-snfromadj  37247  topdifinffinlem  37554  poimirlem9  37832  poimirlem28  37851  poimirlem30  37853  poimirlem32  37855  ftc1cnnc  37895  cncfres  37968  lineset  40066  lautset  40410  pautsetN  40426  tendoset  41087  decpmulnc  42609  decpmul  42610  areaquad  43525  0fno  43743  finonex  43762  sblpnf  44618  lhe4.4ex1a  44637  fourierdlem62  46479  fourierdlem76  46493  lamberte  47201  65537prm  47889  11gbo  48088  bgoldbtbndlem1  48118  seppcld  49242