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

Theorem eqeltrri 2890
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
StepHypRef Expression
1 eqeltrri.1 . . 3 𝐴 = 𝐵
21eqcomi 2810 . 2 𝐵 = 𝐴
3 eqeltrri.2 . 2 𝐴𝐶
42, 3eqeltri 2889 1 𝐵𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2112
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873
This theorem is referenced by:  3eltr3i  2905  zfrep4  5167  p0ex  5253  pp0ex  5255  ord3ex  5256  zfpair  5290  epse  5506  unex  7453  fvresex  7647  opabex3  7654  abexssex  7657  abexex  7658  oprabrexex2  7665  seqomlem3  8075  inf0  9072  scottexs  9304  kardex  9311  infxpenlem  9428  r1om  9659  cfon  9670  fin23lem16  9750  fin1a2lem6  9820  hsmexlem5  9845  brdom7disj  9946  brdom6disj  9947  1lt2pi  10320  0cn  10626  resubcli  10941  0reALT  10976  1nn  11640  10nn  12106  numsucc  12130  nummac  12135  unirnioo  12831  ioorebas  12833  fz0to4untppr  13009  om2uzrani  13319  uzrdg0i  13326  hashunlei  13786  cats1fvn  14215  trclubi  14351  4sqlem19  16292  dec2dvds  16392  mod2xnegi  16400  modsubi  16401  gcdi  16402  isstruct2  16488  grppropstr  18115  nn0srg  20164  ltbval  20714  sn0topon  21606  indistop  21610  indisuni  21611  indistps2  21620  indistps2ALT  21622  restbas  21766  leordtval2  21820  iocpnfordt  21823  icomnfordt  21824  iooordt  21825  reordt  21826  dis1stc  22107  ptcmpfi  22421  ustfn  22810  ustn0  22829  retopbas  23369  blssioo  23403  xrtgioo  23414  zcld  23421  cnperf  23428  retopconn  23437  iimulcn  23546  rembl  24147  mbfdm  24233  ismbf  24235  mbf0  24241  bddiblnc  24448  abelthlem9  25038  advlog  25248  advlogexp  25249  2irrexpq  25324  cxpcn3  25340  loglesqrt  25350  log2ub  25538  ppi1i  25756  cht2  25760  cht3  25761  bpos1lem  25869  lgslem4  25887  vmadivsum  26069  log2sumbnd  26131  selberg2  26138  selbergr  26155  iscgrg  26309  ishpg  26556  ax5seglem7  26732  h2hva  28760  h2hsm  28761  h2hnm  28762  norm-ii-i  28923  hhshsslem2  29054  shincli  29148  chincli  29246  lnophdi  29788  imaelshi  29844  rnelshi  29845  bdophdi  29883  dfdec100  30575  dpadd2  30615  dpmul  30618  dpmul4  30619  nn0omnd  30968  nn0archi  30970  ccfldextrr  31126  lmatfvlem  31168  rmulccn  31279  rrhre  31370  sigaex  31477  br2base  31635  sxbrsigalem3  31638  carsgclctunlem3  31686  sitmcl  31717  rpsqrtcn  31972  hgt750lem  32030  hgt750lem2  32031  afsval  32050  kur14lem7  32567  retopsconn  32604  satfvsuclem1  32714  fmlasuc0  32739  hfuni  33753  neibastop2lem  33816  onint1  33905  topdifinffinlem  34759  poimirlem9  35059  poimirlem28  35078  poimirlem30  35080  poimirlem32  35082  ftc1cnnc  35122  cncfres  35196  lineset  37027  lautset  37371  pautsetN  37387  tendoset  38048  decpmulnc  39468  decpmul  39469  areaquad  40153  sblpnf  41001  lhe4.4ex1a  41020  fourierdlem62  42797  fourierdlem76  42811  65537prm  44080  11gbo  44280  bgoldbtbndlem1  44310
  Copyright terms: Public domain W3C validator