Theorem breqi 5116

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

Syntax hints:   ↔ wb 205   = wceq 1541   class class class wbr 5110

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-br 5111

This theorem is referenced by:  f1ompt  7064  isocnv3  7282  eqfunresadj  7310  brtpos2  8168  brwitnlem  8458  brdifun  8684  omxpenlem  9024  infxpenlem  9958  ltpiord  10832  nqerf  10875  nqerid  10878  ordpinq  10888  ltxrlt  11234  ltxr  13045  trclublem  14892  oduleg  18193  oduposb  18232  join0  18308  meet0  18309  xmeterval  23822  pi1cpbl  24444  slenlt  27137  ltgov  27602  brbtwn  27911  avril1  29470  axhcompl-zf  30003  hlimadd  30198  hhcmpl  30205  hhcms  30208  hlim0  30240  fcoinvbr  31593  brprop  31679  posrasymb  31895  trleile  31901  isarchi  32088  pstmfval  32566  pstmxmet  32567  lmlim  32617  satfbrsuc  34047  brtxp  34541  brpprod  34546  brpprod3b  34548  brtxpsd2  34556  brdomain  34594  brrange  34595  brimg  34598  brapply  34599  brsuccf  34602  brrestrict  34610  brub  34615  brlb  34616  colineardim1  34722  broutsideof  34782  fneval  34900  relowlpssretop  35908  phpreu  36135  poimirlem26  36177  br1cnvres  36802  brid  36840  eqres  36874  alrmomorn  36892  brabidgaw  36899  brabidga  36900  brxrn  36909  br1cossinres  36982  br1cossxrnres  36983  brnonrel  41983  brcofffn  42425  brco2f1o  42426  brco3f1o  42427  clsneikex  42500  clsneinex  42501  clsneiel1  42502  neicvgmex  42511  neicvgel1  42513  climreeq  43974  xlimres  44182  xlimcl  44183  xlimclim  44185  xlimconst  44186  xlimbr  44188  xlimmnfvlem1  44193  xlimmnfvlem2  44194  xlimpnfvlem1  44197  xlimpnfvlem2  44198  xlimuni  44214  gte-lte  47289  gt-lt  47290  gte-lteh  47291  gt-lth  47292