Theorem breqi 5080

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 5076	. 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)

Syntax hints:   ↔ wb 205   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-br 5075

This theorem is referenced by:  f1ompt  6985  isocnv3  7203  brtpos2  8048  brwitnlem  8337  brdifun  8527  omxpenlem  8860  infxpenlem  9769  ltpiord  10643  nqerf  10686  nqerid  10689  ordpinq  10699  ltxrlt  11045  ltxr  12851  trclublem  14706  oduleg  18008  oduposb  18047  join0  18123  meet0  18124  xmeterval  23585  pi1cpbl  24207  ltgov  26958  brbtwn  27267  avril1  28827  axhcompl-zf  29360  hlimadd  29555  hhcmpl  29562  hhcms  29565  hlim0  29597  fcoinvbr  30947  brprop  31030  posrasymb  31243  trleile  31249  isarchi  31436  pstmfval  31846  pstmxmet  31847  lmlim  31897  satfbrsuc  33328  eqfunresadj  33735  slenlt  33955  brtxp  34182  brpprod  34187  brpprod3b  34189  brtxpsd2  34197  brdomain  34235  brrange  34236  brimg  34239  brapply  34240  brsuccf  34243  brrestrict  34251  brub  34256  brlb  34257  colineardim1  34363  broutsideof  34423  fneval  34541  relowlpssretop  35535  phpreu  35761  poimirlem26  35803  brid  36442  eqres  36475  alrmomorn  36490  brabidgaw  36495  brabidga  36496  brxrn  36504  br1cossinres  36565  br1cossxrnres  36566  brnonrel  41197  brcofffn  41641  brco2f1o  41642  brco3f1o  41643  clsneikex  41716  clsneinex  41717  clsneiel1  41718  neicvgmex  41727  neicvgel1  41729  climreeq  43154  xlimres  43362  xlimcl  43363  xlimclim  43365  xlimconst  43366  xlimbr  43368  xlimmnfvlem1  43373  xlimmnfvlem2  43374  xlimpnfvlem1  43377  xlimpnfvlem2  43378  xlimuni  43394  gte-lte  46426  gt-lt  46427  gte-lteh  46428  gt-lth  46429