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

Theorem breqi 4691
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 4687 . 2 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
31, 2ax-mp 5 1 (𝐴𝑅𝐵𝐴𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647  df-br 4686
This theorem is referenced by:  f1ompt  6422  isocnv3  6622  brtpos2  7403  brwitnlem  7632  brdifun  7816  omxpenlem  8102  infxpenlem  8874  ltpiord  9747  nqerf  9790  nqerid  9793  ordpinq  9803  ltxrlt  10146  ltxr  11987  trclublem  13780  oduleg  17179  oduposb  17183  meet0  17184  join0  17185  xmeterval  22284  pi1cpbl  22890  ltgov  25537  brbtwn  25824  rgrprop  26512  rusgrprop  26514  avril1  27449  axhcompl-zf  27983  hlimadd  28178  hhcmpl  28185  hhcms  28188  hlim0  28220  fcoinvbr  29545  posrasymb  29785  trleile  29794  isarchi  29864  pstmfval  30067  pstmxmet  30068  lmlim  30121  eqfunresadj  31785  slenlt  32002  brtxp  32112  brpprod  32117  brpprod3b  32119  brtxpsd2  32127  brdomain  32165  brrange  32166  brimg  32169  brapply  32170  brsuccf  32173  brrestrict  32181  brub  32186  brlb  32187  colineardim1  32293  broutsideof  32353  fneval  32472  relowlpssretop  33342  phpreu  33523  poimirlem26  33565  brid  34218  eqres  34249  alrmomorn  34263  brabidga  34268  brxrn  34276  br1cossinres  34337  br1cossxrnres  34338  brnonrel  38212  brcofffn  38646  brco2f1o  38647  brco3f1o  38648  clsneikex  38721  clsneinex  38722  clsneiel1  38723  neicvgmex  38732  neicvgel1  38734  climreeq  40163  xlimres  40365  xlimcl  40366  xlimclim  40368  xlimconst  40369  xlimbr  40371  xlimmnfvlem1  40376  xlimmnfvlem2  40377  xlimpnfvlem1  40380  xlimpnfvlem2  40381  gte-lte  42793  gt-lt  42794  gte-lteh  42795  gt-lth  42796
  Copyright terms: Public domain W3C validator