Theorem eqeltrri 2825

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  3eltr3i  2840  zfrep4  5232  p0ex  5323  pp0ex  5325  ord3ex  5326  zfpair  5360  epse  5601  unexOLD  7681  fvresex  7895  opabex3  7902  abexssex  7905  abexex  7906  oprabrexex2  7913  seqomlem3  8374  1on  8400  2on  8401  inf0  9517  scottexs  9783  kardex  9790  infxpenlem  9907  r1om  10137  cfon  10149  fin23lem16  10229  fin1a2lem6  10299  hsmexlem5  10324  brdom7disj  10425  brdom6disj  10426  1lt2pi  10799  0cn  11107  resubcli  11426  0reALT  11461  1nn  12139  10nn  12607  numsucc  12631  nummac  12636  unirnioo  13352  ioorebas  13354  om2uzrani  13859  uzrdg0i  13866  hashunlei  14332  cats1fvn  14765  trclubi  14903  4sqlem19  16875  dec2dvds  16975  mod2xnegi  16983  modsubi  16984  gcdi  16985  isstruct2  17060  grppropstr  18832  nn0srg  21344  fermltlchr  21436  ltbval  21948  sn0topon  22883  indistop  22887  indisuni  22888  indistps2  22897  indistps2ALT  22899  restbas  23043  leordtval2  23097  iocpnfordt  23100  icomnfordt  23101  iooordt  23102  reordt  23103  dis1stc  23384  ptcmpfi  23698  ustfn  24087  ustn0  24106  retopbas  24646  blssioo  24681  xrtgioo  24693  zcld  24700  cnperf  24707  retopconn  24716  iimulcnOLD  24833  rembl  25439  mbfdm  25525  ismbf  25527  mbf0  25533  bddiblnc  25741  abelthlem9  26348  advlog  26561  advlogexp  26562  2irrexpq  26638  cxpcn3  26656  loglesqrt  26669  log2ub  26857  ppi1i  27076  cht2  27080  cht3  27081  bpos1lem  27191  lgslem4  27209  vmadivsum  27391  log2sumbnd  27453  selberg2  27460  selbergr  27477  nogt01o  27606  mulsproplem9  28032  1n0s  28245  n0sfincut  28251  2nns  28310  iscgrg  28457  ishpg  28704  ax5seglem7  28880  h2hva  30918  h2hsm  30919  h2hnm  30920  norm-ii-i  31081  hhshsslem2  31212  shincli  31306  chincli  31404  lnophdi  31946  imaelshi  32002  rnelshi  32003  bdophdi  32041  dfdec100  32776  dpadd2  32851  dpmul  32854  dpmul4  32855  nn0omnd  33283  nn0archi  33285  znfermltl  33304  ccfldextrr  33619  lmatfvlem  33788  rrhre  33994  sigaex  34083  br2base  34243  sxbrsigalem3  34246  carsgclctunlem3  34294  sitmcl  34325  rpsqrtcn  34567  hgt750lem  34625  hgt750lem2  34626  afsval  34645  kur14lem7  35195  retopsconn  35232  satfvsuclem1  35342  fmlasuc0  35367  hfuni  36168  neibastop2lem  36344  onint1  36433  bj-snfromadj  37028  topdifinffinlem  37331  poimirlem9  37619  poimirlem28  37638  poimirlem30  37640  poimirlem32  37642  ftc1cnnc  37682  cncfres  37755  lineset  39727  lautset  40071  pautsetN  40087  tendoset  40748  decpmulnc  42270  decpmul  42271  areaquad  43199  0no  43418  finonex  43437  sblpnf  44293  lhe4.4ex1a  44312  fourierdlem62  46159  fourierdlem76  46173  lamberte  46882  65537prm  47570  11gbo  47769  bgoldbtbndlem1  47799  seppcld  48924