Theorem breqi 5108

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

Step	Hyp	Ref	Expression
1		breqi.1	. 2 ⊢ 𝑅 = 𝑆
2		breq 5104	. 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)

Syntax hints:   ↔ wb 208   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839  df-br 5103

This theorem is referenced by:  f1ompt  7094  isocnv3  7318  eqfunresadj  7346  brtpos2  8214  brwitnlem  8478  brdifun  8711  omxpenlem  9052  infxpenlem  9971  ltpiord  10847  nqerf  10890  nqerid  10893  ordpinq  10903  ltxrlt  11255  ltxr  13119  trclublem  15010  oduleg  18324  oduposb  18361  join0  18437  meet0  18438  xmeterval  24494  pi1cpbl  25108  lenlts  27818  ltgov  28768  brbtwn  29102  avril1  30667  axhcompl-zf  31203  hlimadd  31398  hhcmpl  31405  hhcms  31408  hlim0  31440  fcoinvbr  32807  brprop  32901  posrasymb  33147  trleile  33151  isarchi  33364  pstmfval  34195  pstmxmet  34196  lmlim  34246  morleylemrneab  34967  fineqvnttrclse  35424  satfbrsuc  35721  brtxp  36233  brpprod  36238  brpprod3b  36240  brtxpsd2  36248  brdomain  36286  brrange  36287  brimg  36290  brapply  36291  brsuccf  36295  brrestrict  36304  brub  36309  brlb  36310  colineardim1  36416  broutsideof  36476  fneval  36717  relowlpssretop  37863  phpreu  38108  poimirlem26  38150  br1cnvres  38778  brid  38816  eqres  38844  alrmomorn  38862  brabidgaw  38877  brabidga  38878  brxrn  38887  br1cossinres  39041  br1cossxrnres  39042  brnonrel  44170  brcofffn  44612  brco2f1o  44613  brco3f1o  44614  clsneikex  44687  clsneinex  44688  clsneiel1  44689  neicvgmex  44698  neicvgel1  44700  brpermmodel  45584  climreeq  46194  xlimres  46400  xlimcl  46401  xlimclim  46403  xlimconst  46404  xlimbr  46406  xlimmnfvlem1  46411  xlimmnfvlem2  46412  xlimpnfvlem1  46415  xlimpnfvlem2  46416  xlimuni  46432  lambert0  47486  lamberte  47487  islmd  50291  iscmd  50292  lmdran  50297  cmdlan  50298  gte-lte  50350  gt-lt  50351  gte-lteh  50352  gt-lth  50353