Theorem eqeltrri 2861

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  3eltr3i  2876  zfrep4  5249  p0ex  5350  pp0ex  5352  ord3ex  5353  zfpair  5387  moabex  5430  epse  5637  fvresex  7993  opabex3  8000  abexssex  8003  abexex  8004  oprabrexex2  8011  seqomlem3  8487  1on  8514  2on  8515  inf0  9646  hfuniOLD  9949  scottexsOLD  9967  kardexOLD  9982  infxpenlem  10116  cfonOLD  10357  fin23lem16  10437  fin1a2lem6  10507  hsmexlem5  10532  brdom7disj  10634  brdom6disj  10635  1lt2pi  11014  0cn  11322  resubcli  11644  0reALT  11679  1nn  12370  10nn  12858  numsucc  12883  nummac  12888  unirnioo  13604  ioorebas  13606  om2uzrani  14119  uzrdg0i  14126  hashunlei  14594  cats1fvn  15034  trclubi  15175  sgnrn  15277  4sqlem19  17167  dec2dvds  17267  mod2xnegi  17275  modsubi  17276  gcdi  17277  isstruct2  17353  smndex1gbas  19124  smndex1gid  19126  smndex1igid  19128  grppropstr  19190  nn0srg  21770  fermltlchr  21862  ltbval  22379  sn0topon  23343  indistop  23347  indisuni  23348  indistps2  23357  indistps2ALT  23359  restbas  23503  leordtval2  23557  iocpnfordt  23560  icomnfordt  23561  iooordt  23562  reordt  23563  dis1stc  23845  ptcmpfi  24159  ustfn  24548  ustn0  24567  retopbas  25106  blssioo  25141  xrtgioo  25153  zcld  25160  cnperf  25167  retopconn  25176  rembl  25888  mbfdm  25974  ismbf  25976  mbf0  25982  bddiblnc  26189  abelthlem9  26794  advlog  27009  advlogexp  27010  2irrexpq  27086  cxpcn3  27103  loglesqrt  27116  log2ub  27304  ppi1i  27522  cht2  27526  cht3  27527  bpos1lem  27636  lgslem4  27654  vmadivsum  27836  log2sumbnd  27898  selberg2  27905  selbergr  27922  nogt01o  28080  mulsproplem9  28537  1n0s  28761  n0fincut  28768  2nns  28831  istrkg2ld  28949  iscgrg  29002  ishpg  29264  ax5seglem7  29540  h2hva  31603  h2hsm  31604  h2hnm  31605  norm-ii-i  31766  hhshsslem2  31897  shincli  31991  chincli  32089  lnophdi  32631  imaelshi  32687  rnelshi  32688  bdophdi  32726  padct  33378  dfdec100  33488  dpadd2  33543  dpmul  33546  dpmul4  33547  nn0omnd  33972  nn0archi  33975  znfermltl  33989  ccfldextrr  34345  lmatfvlem  34514  rrhre  34720  sigaex  34809  br2base  34968  sxbrsigalem3  34971  carsgclctunlem3  35019  sitmcl  35050  rpsqrtcn  35289  hgt750lem  35347  hgt750lem2  35348  afsval  35370  kur14lem7  36143  retopsconn  36180  satfvsuclem1  36290  fmlasuc0  36315  neibastop2lem  37325  onint1  37414  ttcid  37457  bj-snfromadj  38134  topdifinffinlem  38461  poimirlem9  38738  poimirlem28  38757  poimirlem30  38759  poimirlem32  38761  ftc1cnnc  38801  dfproplem  38832  cncfres  38890  scottexf  39291  lineset  40986  lautset  41330  pautsetN  41346  tendoset  42007  decpmulnc  43535  decpmul  43536  areaquad  44408  0fno  44626  finonex  44645  sblpnf  45484  lhe4.4ex1a  45503  fourierdlem62  47381  fourierdlem76  47395  lamberte  48141  65537prm  48864  11gbo  49076  bgoldbtbndlem1  49106  seppcld  50247  setc1onsubc  50943