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

Theorem breqi 4810
Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
Hypothesis
Ref Expression
breqi.1 𝑅 = 𝑆
Assertion
Ref Expression
breqi (𝐴𝑅𝐵𝐴𝑆𝐵)

Proof of Theorem breqi
StepHypRef Expression
1 breqi.1 . 2 𝑅 = 𝑆
2 breq 4806 . 2 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
31, 2ax-mp 5 1 (𝐴𝑅𝐵𝐴𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1632   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-clel 2756  df-br 4805
This theorem is referenced by:  f1ompt  6546  isocnv3  6746  brtpos2  7528  brwitnlem  7758  brdifun  7942  omxpenlem  8228  infxpenlem  9046  ltpiord  9921  nqerf  9964  nqerid  9967  ordpinq  9977  ltxrlt  10320  ltxr  12162  trclublem  13955  oduleg  17353  oduposb  17357  meet0  17358  join0  17359  xmeterval  22458  pi1cpbl  23064  ltgov  25712  brbtwn  25999  rgrprop  26687  rusgrprop  26689  avril1  27651  axhcompl-zf  28185  hlimadd  28380  hhcmpl  28387  hhcms  28390  hlim0  28422  fcoinvbr  29747  posrasymb  29987  trleile  29996  isarchi  30066  pstmfval  30269  pstmxmet  30270  lmlim  30323  eqfunresadj  31987  slenlt  32204  brtxp  32314  brpprod  32319  brpprod3b  32321  brtxpsd2  32329  brdomain  32367  brrange  32368  brimg  32371  brapply  32372  brsuccf  32375  brrestrict  32383  brub  32388  brlb  32389  colineardim1  32495  broutsideof  32555  fneval  32674  relowlpssretop  33541  phpreu  33724  poimirlem26  33766  brid  34419  eqres  34450  alrmomorn  34464  brabidga  34469  brxrn  34477  br1cossinres  34538  br1cossxrnres  34539  brnonrel  38415  brcofffn  38849  brco2f1o  38850  brco3f1o  38851  clsneikex  38924  clsneinex  38925  clsneiel1  38926  neicvgmex  38935  neicvgel1  38937  climreeq  40366  xlimres  40568  xlimcl  40569  xlimclim  40571  xlimconst  40572  xlimbr  40574  xlimmnfvlem1  40579  xlimmnfvlem2  40580  xlimpnfvlem1  40583  xlimpnfvlem2  40584  gte-lte  42996  gt-lt  42997  gte-lteh  42998  gt-lth  42999
  Copyright terms: Public domain W3C validator