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

Theorem breqi 4583
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 4579 . 2 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
31, 2ax-mp 5 1 (𝐴𝑅𝐵𝐴𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474   class class class wbr 4577
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-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605  df-br 4578
This theorem is referenced by:  f1ompt  6274  isocnv3  6459  brtpos2  7222  brwitnlem  7451  brdifun  7635  omxpenlem  7923  infxpenlem  8696  ltpiord  9565  nqerf  9608  nqerid  9611  ordpinq  9621  ltxrlt  9959  ltxr  11786  trclublem  13530  oduleg  16903  oduposb  16907  meet0  16908  join0  16909  xmeterval  21994  pi1cpbl  22599  ltgov  25237  brbtwn  25524  rgraprop  26248  rusgraprop  26249  rusgrargra  26250  avril1  26504  axhcompl-zf  27032  hlimadd  27227  hhcmpl  27234  hhcms  27237  hlim0  27269  fcoinvbr  28592  posrasymb  28781  trleile  28790  isarchi  28860  pstmfval  29060  pstmxmet  29061  lmlim  29114  brtxp  30950  brpprod  30955  brpprod3b  30957  brtxpsd2  30965  brdomain  31003  brrange  31004  brimg  31007  brapply  31008  brsuccf  31011  brrestrict  31019  brub  31024  brlb  31025  colineardim1  31131  broutsideof  31191  fneval  31310  relowlpssretop  32171  phpreu  32346  poimirlem26  32388  brnonrel  36697  brcofffn  37132  brco2f1o  37133  brco3f1o  37134  clsneikex  37207  clsneinex  37208  clsneiel1  37209  neicvgmex  37218  neicvgel1  37220  climreeq  38463  rgrprop  40741  rusgrprop  40743  gte-lte  42206  gt-lt  42207  gte-lteh  42208  gt-lth  42209
  Copyright terms: Public domain W3C validator