Theorem eqeltrri 2835

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

Syntax hints:   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  3eltr3i  2850  zfrep4  5298  p0ex  5389  pp0ex  5391  ord3ex  5392  zfpair  5426  epse  5670  unexOLD  7763  fvresex  7982  opabex3  7990  abexssex  7993  abexex  7994  oprabrexex2  8001  seqomlem3  8490  1on  8516  2on  8518  inf0  9658  scottexs  9924  kardex  9931  infxpenlem  10050  r1om  10280  cfon  10292  fin23lem16  10372  fin1a2lem6  10442  hsmexlem5  10467  brdom7disj  10568  brdom6disj  10569  1lt2pi  10942  0cn  11250  resubcli  11568  0reALT  11603  1nn  12274  10nn  12746  numsucc  12770  nummac  12775  unirnioo  13485  ioorebas  13487  om2uzrani  13989  uzrdg0i  13996  hashunlei  14460  cats1fvn  14893  trclubi  15031  4sqlem19  16996  dec2dvds  17096  mod2xnegi  17104  modsubi  17105  gcdi  17106  isstruct2  17182  grppropstr  18983  nn0srg  21472  fermltlchr  21561  ltbval  22078  sn0topon  23020  indistop  23024  indisuni  23025  indistps2  23034  indistps2ALT  23037  restbas  23181  leordtval2  23235  iocpnfordt  23238  icomnfordt  23239  iooordt  23240  reordt  23241  dis1stc  23522  ptcmpfi  23836  ustfn  24225  ustn0  24244  retopbas  24796  blssioo  24830  xrtgioo  24841  zcld  24848  cnperf  24855  retopconn  24864  iimulcnOLD  24981  rembl  25588  mbfdm  25674  ismbf  25676  mbf0  25682  bddiblnc  25891  abelthlem9  26498  advlog  26710  advlogexp  26711  2irrexpq  26787  cxpcn3  26805  loglesqrt  26818  log2ub  27006  ppi1i  27225  cht2  27229  cht3  27230  bpos1lem  27340  lgslem4  27358  vmadivsum  27540  log2sumbnd  27602  selberg2  27609  selbergr  27626  nogt01o  27755  mulsproplem9  28164  1n0s  28365  2nns  28416  iscgrg  28534  ishpg  28781  ax5seglem7  28964  h2hva  31002  h2hsm  31003  h2hnm  31004  norm-ii-i  31165  hhshsslem2  31296  shincli  31390  chincli  31488  lnophdi  32030  imaelshi  32086  rnelshi  32087  bdophdi  32125  dfdec100  32836  dpadd2  32876  dpmul  32879  dpmul4  32880  nn0omnd  33352  nn0archi  33354  znfermltl  33373  ccfldextrr  33675  lmatfvlem  33775  rrhre  33983  sigaex  34090  br2base  34250  sxbrsigalem3  34253  carsgclctunlem3  34301  sitmcl  34332  rpsqrtcn  34586  hgt750lem  34644  hgt750lem2  34645  afsval  34664  kur14lem7  35196  retopsconn  35233  satfvsuclem1  35343  fmlasuc0  35368  hfuni  36165  neibastop2lem  36342  onint1  36431  bj-snfromadj  37026  topdifinffinlem  37329  poimirlem9  37615  poimirlem28  37634  poimirlem30  37636  poimirlem32  37638  ftc1cnnc  37678  cncfres  37751  lineset  39720  lautset  40064  pautsetN  40080  tendoset  40741  decpmulnc  42300  decpmul  42301  areaquad  43204  0no  43424  finonex  43443  sblpnf  44305  lhe4.4ex1a  44324  fourierdlem62  46123  fourierdlem76  46137  65537prm  47500  11gbo  47699  bgoldbtbndlem1  47729  seppcld  48725