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  5228  p0ex  5319  pp0ex  5321  ord3ex  5322  zfpair  5356  moabex  5403  epse  5604  unexOLD  7690  fvresex  7904  opabex3  7911  abexssex  7914  abexex  7915  oprabrexex2  7922  seqomlem3  8382  1on  8408  2on  8409  inf0  9531  scottexs  9800  kardex  9807  infxpenlem  9924  r1om  10154  cfon  10166  fin23lem16  10246  fin1a2lem6  10316  hsmexlem5  10341  brdom7disj  10442  brdom6disj  10443  1lt2pi  10817  0cn  11125  resubcli  11444  0reALT  11479  1nn  12157  10nn  12624  numsucc  12648  nummac  12653  unirnioo  13366  ioorebas  13368  om2uzrani  13876  uzrdg0i  13883  hashunlei  14349  cats1fvn  14782  trclubi  14920  4sqlem19  16892  dec2dvds  16992  mod2xnegi  17000  modsubi  17001  gcdi  17002  isstruct2  17077  smndex1gbas  18828  smndex1gid  18830  smndex1igid  18832  grppropstr  18887  nn0srg  21394  fermltlchr  21486  ltbval  21999  sn0topon  22941  indistop  22945  indisuni  22946  indistps2  22955  indistps2ALT  22957  restbas  23101  leordtval2  23155  iocpnfordt  23158  icomnfordt  23159  iooordt  23160  reordt  23161  dis1stc  23442  ptcmpfi  23756  ustfn  24145  ustn0  24164  retopbas  24703  blssioo  24738  xrtgioo  24750  zcld  24757  cnperf  24764  retopconn  24773  rembl  25485  mbfdm  25571  ismbf  25573  mbf0  25579  bddiblnc  25787  abelthlem9  26390  advlog  26603  advlogexp  26604  2irrexpq  26680  cxpcn3  26698  loglesqrt  26711  log2ub  26899  ppi1i  27118  cht2  27122  cht3  27123  bpos1lem  27233  lgslem4  27251  vmadivsum  27433  log2sumbnd  27495  selberg2  27502  selbergr  27519  nogt01o  27648  mulsproplem9  28104  1n0s  28328  n0fincut  28335  2nns  28398  istrkg2ld  28516  iscgrg  28568  ishpg  28815  ax5seglem7  28992  h2hva  31034  h2hsm  31035  h2hnm  31036  norm-ii-i  31197  hhshsslem2  31328  shincli  31422  chincli  31520  lnophdi  32062  imaelshi  32118  rnelshi  32119  bdophdi  32157  padct  32780  dfdec100  32894  dpadd2  32974  dpmul  32977  dpmul4  32978  nn0omnd  33409  nn0archi  33412  znfermltl  33431  ccfldextrr  33796  lmatfvlem  33965  rrhre  34171  sigaex  34260  br2base  34419  sxbrsigalem3  34422  carsgclctunlem3  34470  sitmcl  34501  rpsqrtcn  34743  hgt750lem  34801  hgt750lem2  34802  afsval  34821  kur14lem7  35400  retopsconn  35437  satfvsuclem1  35547  fmlasuc0  35572  hfuni  36372  neibastop2lem  36548  onint1  36637  ttcid  36680  bj-snfromadj  37349  topdifinffinlem  37659  poimirlem9  37941  poimirlem28  37960  poimirlem30  37962  poimirlem32  37964  ftc1cnnc  38004  cncfres  38077  lineset  40175  lautset  40519  pautsetN  40535  tendoset  41196  decpmulnc  42718  decpmul  42719  areaquad  43647  0fno  43865  finonex  43884  sblpnf  44740  lhe4.4ex1a  44759  fourierdlem62  46600  fourierdlem76  46614  lamberte  47322  65537prm  48010  11gbo  48209  bgoldbtbndlem1  48239  seppcld  49363