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

Theorem breqi 4846
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 4842 . 2 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
31, 2ax-mp 5 1 (𝐴𝑅𝐵𝐴𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637   class class class wbr 4840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2798  df-clel 2801  df-br 4841
This theorem is referenced by:  f1ompt  6600  isocnv3  6803  brtpos2  7590  brwitnlem  7821  brdifun  8005  omxpenlem  8297  infxpenlem  9116  ltpiord  9991  nqerf  10034  nqerid  10037  ordpinq  10047  ltxrlt  10390  ltxr  12161  trclublem  13955  oduleg  17333  oduposb  17337  meet0  17338  join0  17339  xmeterval  22446  pi1cpbl  23052  ltgov  25702  brbtwn  25989  rgrprop  26680  rusgrprop  26682  avril1  27646  axhcompl-zf  28180  hlimadd  28375  hhcmpl  28382  hhcms  28385  hlim0  28417  fcoinvbr  29741  posrasymb  29979  trleile  29988  isarchi  30058  pstmfval  30261  pstmxmet  30262  lmlim  30315  eqfunresadj  31978  slenlt  32195  brtxp  32305  brpprod  32310  brpprod3b  32312  brtxpsd2  32320  brdomain  32358  brrange  32359  brimg  32362  brapply  32363  brsuccf  32366  brrestrict  32374  brub  32379  brlb  32380  colineardim1  32486  broutsideof  32546  fneval  32665  relowlpssretop  33525  phpreu  33703  poimirlem26  33745  brid  34390  eqres  34420  alrmomorn  34433  brabidga  34438  brxrn  34446  br1cossinres  34507  br1cossxrnres  34508  brnonrel  38392  brcofffn  38826  brco2f1o  38827  brco3f1o  38828  clsneikex  38901  clsneinex  38902  clsneiel1  38903  neicvgmex  38912  neicvgel1  38914  climreeq  40322  xlimres  40524  xlimcl  40525  xlimclim  40527  xlimconst  40528  xlimbr  40530  xlimmnfvlem1  40535  xlimmnfvlem2  40536  xlimpnfvlem1  40539  xlimpnfvlem2  40540  gte-lte  43033  gt-lt  43034  gte-lteh  43035  gt-lth  43036
  Copyright terms: Public domain W3C validator