Theorem eqeltrri 2838

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

Syntax hints:   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  3eltr3i  2853  zfrep4  5218  p0ex  5316  pp0ex  5318  ord3ex  5319  zfpair  5353  moabex  5400  epse  5603  unexOLD  7692  fvresex  7906  opabex3  7913  abexssex  7916  abexex  7917  oprabrexex2  7924  seqomlem3  8385  1on  8411  2on  8412  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  21416  fermltlchr  21508  ltbval  22023  sn0topon  22985  indistop  22989  indisuni  22990  indistps2  22999  indistps2ALT  23001  restbas  23145  leordtval2  23199  iocpnfordt  23202  icomnfordt  23203  iooordt  23204  reordt  23205  dis1stc  23486  ptcmpfi  23800  ustfn  24189  ustn0  24208  retopbas  24747  blssioo  24782  xrtgioo  24794  zcld  24801  cnperf  24808  retopconn  24817  rembl  25529  mbfdm  25615  ismbf  25617  mbf0  25623  bddiblnc  25831  abelthlem9  26427  advlog  26640  advlogexp  26641  2irrexpq  26717  cxpcn3  26734  loglesqrt  26747  log2ub  26935  ppi1i  27153  cht2  27157  cht3  27158  bpos1lem  27267  lgslem4  27285  vmadivsum  27467  log2sumbnd  27529  selberg2  27536  selbergr  27553  nogt01o  27682  mulsproplem9  28138  1n0s  28362  n0fincut  28369  2nns  28432  istrkg2ld  28550  iscgrg  28602  ishpg  28849  ax5seglem7  29026  h2hva  31067  h2hsm  31068  h2hnm  31069  norm-ii-i  31230  hhshsslem2  31361  shincli  31455  chincli  31553  lnophdi  32095  imaelshi  32151  rnelshi  32152  bdophdi  32190  padct  32814  dfdec100  32926  dpadd2  32992  dpmul  32995  dpmul4  32996  nn0omnd  33431  nn0archi  33434  znfermltl  33453  ccfldextrr  33842  lmatfvlem  34011  rrhre  34217  sigaex  34306  br2base  34465  sxbrsigalem3  34468  carsgclctunlem3  34516  sitmcl  34547  rpsqrtcn  34789  hgt750lem  34847  hgt750lem2  34848  afsval  34870  kur14lem7  35455  retopsconn  35492  satfvsuclem1  35602  fmlasuc0  35627  hfuni  36427  neibastop2lem  36603  onint1  36692  ttcid  36735  bj-snfromadj  37412  topdifinffinlem  37724  poimirlem9  38011  poimirlem28  38030  poimirlem30  38032  poimirlem32  38034  ftc1cnnc  38074  cncfres  38147  lineset  40245  lautset  40589  pautsetN  40605  tendoset  41266  decpmulnc  42779  decpmul  42780  areaquad  43676  0fno  43894  finonex  43913  sblpnf  44769  lhe4.4ex1a  44788  fourierdlem62  46625  fourierdlem76  46639  lamberte  47365  65537prm  48068  11gbo  48280  bgoldbtbndlem1  48310  seppcld  49434  setc1onsubc  50106