Theorem breqi 5172

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

Syntax hints:   ↔ wb 206   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-br 5167

This theorem is referenced by:  f1ompt  7145  isocnv3  7368  eqfunresadj  7396  brtpos2  8273  brwitnlem  8563  brdifun  8793  omxpenlem  9139  infxpenlem  10082  ltpiord  10956  nqerf  10999  nqerid  11002  ordpinq  11012  ltxrlt  11360  ltxr  13178  trclublem  15044  oduleg  18360  oduposb  18399  join0  18475  meet0  18476  xmeterval  24463  pi1cpbl  25096  slenlt  27815  ltgov  28623  brbtwn  28932  avril1  30495  axhcompl-zf  31030  hlimadd  31225  hhcmpl  31232  hhcms  31235  hlim0  31267  fcoinvbr  32627  brprop  32709  posrasymb  32938  trleile  32944  isarchi  33162  pstmfval  33842  pstmxmet  33843  lmlim  33893  satfbrsuc  35334  brtxp  35844  brpprod  35849  brpprod3b  35851  brtxpsd2  35859  brdomain  35897  brrange  35898  brimg  35901  brapply  35902  brsuccf  35905  brrestrict  35913  brub  35918  brlb  35919  colineardim1  36025  broutsideof  36085  fneval  36318  relowlpssretop  37330  phpreu  37564  poimirlem26  37606  br1cnvres  38225  brid  38262  eqres  38296  alrmomorn  38314  brabidgaw  38321  brabidga  38322  brxrn  38330  br1cossinres  38403  br1cossxrnres  38404  brnonrel  43551  brcofffn  43993  brco2f1o  43994  brco3f1o  43995  clsneikex  44068  clsneinex  44069  clsneiel1  44070  neicvgmex  44079  neicvgel1  44081  climreeq  45534  xlimres  45742  xlimcl  45743  xlimclim  45745  xlimconst  45746  xlimbr  45748  xlimmnfvlem1  45753  xlimmnfvlem2  45754  xlimpnfvlem1  45757  xlimpnfvlem2  45758  xlimuni  45774  gte-lte  48816  gt-lt  48817  gte-lteh  48818  gt-lth  48819