Theorem eqeltrri 2857

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  3eltr3i  2872  zfrep4  5245  p0ex  5345  pp0ex  5347  ord3ex  5348  zfpair  5382  moabex  5425  epse  5632  fvresex  7972  opabex3  7979  abexssex  7982  abexex  7983  oprabrexex2  7990  seqomlem3  8462  1on  8489  2on  8490  inf0  9622  hfuniOLD  9925  scottexsOLD  9943  kardexOLD  9958  infxpenlem  10092  cfonOLD  10333  fin23lem16  10413  fin1a2lem6  10483  hsmexlem5  10508  brdom7disj  10610  brdom6disj  10611  1lt2pi  10990  0cn  11298  resubcli  11620  0reALT  11655  1nn  12346  10nn  12834  numsucc  12859  nummac  12864  unirnioo  13580  ioorebas  13582  om2uzrani  14095  uzrdg0i  14102  hashunlei  14570  cats1fvn  15009  trclubi  15149  sgnrn  15251  4sqlem19  17141  dec2dvds  17241  mod2xnegi  17249  modsubi  17250  gcdi  17251  isstruct2  17327  smndex1gbas  19098  smndex1gid  19100  smndex1igid  19102  grppropstr  19164  nn0srg  21743  fermltlchr  21835  ltbval  22352  sn0topon  23316  indistop  23320  indisuni  23321  indistps2  23330  indistps2ALT  23332  restbas  23476  leordtval2  23530  iocpnfordt  23533  icomnfordt  23534  iooordt  23535  reordt  23536  dis1stc  23818  ptcmpfi  24132  ustfn  24521  ustn0  24540  retopbas  25079  blssioo  25114  xrtgioo  25126  zcld  25133  cnperf  25140  retopconn  25149  rembl  25861  mbfdm  25947  ismbf  25949  mbf0  25955  bddiblnc  26162  abelthlem9  26767  advlog  26982  advlogexp  26983  2irrexpq  27059  cxpcn3  27076  loglesqrt  27089  log2ub  27277  ppi1i  27495  cht2  27499  cht3  27500  bpos1lem  27609  lgslem4  27627  vmadivsum  27809  log2sumbnd  27871  selberg2  27878  selbergr  27895  nogt01o  28053  mulsproplem9  28510  1n0s  28734  n0fincut  28741  2nns  28804  istrkg2ld  28922  iscgrg  28975  ishpg  29237  ax5seglem7  29513  h2hva  31576  h2hsm  31577  h2hnm  31578  norm-ii-i  31739  hhshsslem2  31870  shincli  31964  chincli  32062  lnophdi  32604  imaelshi  32660  rnelshi  32661  bdophdi  32699  padct  33310  dfdec100  33421  dpadd2  33476  dpmul  33479  dpmul4  33480  nn0omnd  33905  nn0archi  33908  znfermltl  33922  ccfldextrr  34278  lmatfvlem  34447  rrhre  34653  sigaex  34742  br2base  34901  sxbrsigalem3  34904  carsgclctunlem3  34952  sitmcl  34983  rpsqrtcn  35222  hgt750lem  35280  hgt750lem2  35281  afsval  35303  kur14lem7  35977  retopsconn  36014  satfvsuclem1  36124  fmlasuc0  36149  neibastop2lem  37148  onint1  37237  ttcid  37280  bj-snfromadj  37957  topdifinffinlem  38271  poimirlem9  38548  poimirlem28  38567  poimirlem30  38569  poimirlem32  38571  ftc1cnnc  38611  dfproplem  38642  cncfres  38700  scottexf  39101  lineset  40796  lautset  41140  pautsetN  41156  tendoset  41817  decpmulnc  43345  decpmul  43346  areaquad  44218  0fno  44436  finonex  44455  sblpnf  45294  lhe4.4ex1a  45313  fourierdlem62  47178  fourierdlem76  47192  lamberte  47938  65537prm  48661  11gbo  48873  bgoldbtbndlem1  48903  seppcld  50038  setc1onsubc  50710