MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltrri Structured version   Visualization version   GIF version

Theorem eqeltrri 2684
Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
eqeltrr.1 𝐴 = 𝐵
eqeltrr.2 𝐴𝐶
Assertion
Ref Expression
eqeltrri 𝐵𝐶

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3 𝐴 = 𝐵
21eqcomi 2618 . 2 𝐵 = 𝐴
3 eqeltrr.2 . 2 𝐴𝐶
42, 3eqeltri 2683 1 𝐵𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  3eltr3i  2699  zfrep4  4701  p0ex  4773  pp0ex  4775  ord3ex  4776  zfpair  4825  epse  5010  unex  6831  fvresex  7009  abrexex  7010  opabex3  7015  abrexex2  7017  abexssex  7018  abexex  7019  oprabrexex2  7026  seqomlem3  7411  inf0  8378  scottexs  8610  kardex  8617  infxpenlem  8696  r1om  8926  cfon  8937  fin23lem16  9017  fin1a2lem6  9087  hsmexlem5  9112  brdom7disj  9211  brdom6disj  9212  1lt2pi  9583  0cn  9888  resubcli  10194  0reALT  10229  1nn  10880  10nn  11348  numsucc  11383  nummac  11392  unirnioo  12102  ioorebas  12104  fz0to4untppr  12268  om2uzrani  12570  uzrdg0i  12577  hashunlei  13026  cats1fvn  13402  trclubi  13531  trclubiOLD  13532  4sqlem19  15453  dec2dvds  15553  mod2xnegi  15561  modsubi  15562  gcdi  15563  isstruct2  15652  grppropstr  17210  ltbval  19240  nn0srg  19583  sn0topon  20559  indistop  20563  indisuni  20564  indistps2  20573  indistps2ALT  20575  restbas  20719  leordtval2  20773  iocpnfordt  20776  icomnfordt  20777  iooordt  20778  reordt  20779  dis1stc  21059  ptcmpfi  21373  ustfn  21762  ustn0  21781  retopbas  22321  blssioo  22353  xrtgioo  22364  zcld  22371  cnperf  22378  retopcon  22387  iimulcn  22492  rembl  23059  mbfdm  23145  ismbf  23147  abelthlem9  23942  advlog  24144  advlogexp  24145  cxpcn3  24233  loglesqrt  24243  log2ub  24420  ppi1i  24638  cht2  24642  cht3  24643  bpos1lem  24751  lgslem4  24769  vmadivsum  24915  log2sumbnd  24977  selberg2  24984  selbergr  25001  iscgrg  25152  ishpg  25396  ax5seglem7  25560  iseupa  26285  h2hva  27008  h2hsm  27009  h2hnm  27010  norm-ii-i  27171  hhshsslem2  27302  shincli  27398  chincli  27496  lnophdi  28038  imaelshi  28094  rnelshi  28095  bdophdi  28133  nn0omnd  28965  nn0archi  28967  lmatfvlem  29002  rmulccn  29095  rrhre  29186  sigaex  29292  br2base  29451  sxbrsigalem3  29454  carsgclctunlem3  29502  sitmcl  29533  afsval  29795  kur14lem7  30241  retopscon  30278  hfuni  31254  neibastop2lem  31318  onint1  31411  topdifinffinlem  32154  poimirlem9  32371  poimirlem28  32390  poimirlem30  32392  poimirlem32  32394  0mbf  32408  bddiblnc  32433  ftc1cnnc  32437  cncfres  32517  lineset  33825  lautset  34169  pautsetN  34185  tendoset  34848  areaquad  36604  sblpnf  37314  lhe4.4ex1a  37333  fourierdlem62  38844  fourierdlem76  38858  65537prm  39810  11gboa  39981  bgoldbtbndlem1  40005  fusgrfis  40530
  Copyright terms: Public domain W3C validator