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  5229  p0ex  5323  pp0ex  5325  ord3ex  5326  zfpair  5360  moabex  5407  epse  5608  unexOLD  7694  fvresex  7908  opabex3  7915  abexssex  7918  abexex  7919  oprabrexex2  7926  seqomlem3  8386  1on  8412  2on  8413  inf0  9537  scottexs  9806  kardex  9813  infxpenlem  9930  r1om  10160  cfon  10172  fin23lem16  10252  fin1a2lem6  10322  hsmexlem5  10347  brdom7disj  10448  brdom6disj  10449  1lt2pi  10823  0cn  11131  resubcli  11451  0reALT  11486  1nn  12180  10nn  12655  numsucc  12679  nummac  12684  unirnioo  13397  ioorebas  13399  om2uzrani  13909  uzrdg0i  13916  hashunlei  14382  cats1fvn  14815  trclubi  14953  4sqlem19  16929  dec2dvds  17029  mod2xnegi  17037  modsubi  17038  gcdi  17039  isstruct2  17114  smndex1gbas  18865  smndex1gid  18867  smndex1igid  18869  grppropstr  18924  nn0srg  21431  fermltlchr  21523  ltbval  22035  sn0topon  22977  indistop  22981  indisuni  22982  indistps2  22991  indistps2ALT  22993  restbas  23137  leordtval2  23191  iocpnfordt  23194  icomnfordt  23195  iooordt  23196  reordt  23197  dis1stc  23478  ptcmpfi  23792  ustfn  24181  ustn0  24200  retopbas  24739  blssioo  24774  xrtgioo  24786  zcld  24793  cnperf  24800  retopconn  24809  rembl  25521  mbfdm  25607  ismbf  25609  mbf0  25615  bddiblnc  25823  abelthlem9  26422  advlog  26635  advlogexp  26636  2irrexpq  26712  cxpcn3  26729  loglesqrt  26742  log2ub  26930  ppi1i  27149  cht2  27153  cht3  27154  bpos1lem  27263  lgslem4  27281  vmadivsum  27463  log2sumbnd  27525  selberg2  27532  selbergr  27549  nogt01o  27678  mulsproplem9  28134  1n0s  28358  n0fincut  28365  2nns  28428  istrkg2ld  28546  iscgrg  28598  ishpg  28845  ax5seglem7  29022  h2hva  31064  h2hsm  31065  h2hnm  31066  norm-ii-i  31227  hhshsslem2  31358  shincli  31452  chincli  31550  lnophdi  32092  imaelshi  32148  rnelshi  32149  bdophdi  32187  padct  32810  dfdec100  32922  dpadd2  32988  dpmul  32991  dpmul4  32992  nn0omnd  33423  nn0archi  33426  znfermltl  33445  ccfldextrr  33810  lmatfvlem  33979  rrhre  34185  sigaex  34274  br2base  34433  sxbrsigalem3  34436  carsgclctunlem3  34484  sitmcl  34515  rpsqrtcn  34757  hgt750lem  34815  hgt750lem2  34816  afsval  34835  kur14lem7  35414  retopsconn  35451  satfvsuclem1  35561  fmlasuc0  35586  hfuni  36386  neibastop2lem  36562  onint1  36651  ttcid  36694  bj-snfromadj  37371  topdifinffinlem  37681  poimirlem9  37968  poimirlem28  37987  poimirlem30  37989  poimirlem32  37991  ftc1cnnc  38031  cncfres  38104  lineset  40202  lautset  40546  pautsetN  40562  tendoset  41223  decpmulnc  42737  decpmul  42738  areaquad  43666  0fno  43884  finonex  43903  sblpnf  44759  lhe4.4ex1a  44778  fourierdlem62  46618  fourierdlem76  46632  lamberte  47352  65537prm  48055  11gbo  48267  bgoldbtbndlem1  48297  seppcld  49421  setc1onsubc  50093