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 206   = wceq 1540   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-br 5111

This theorem is referenced by:  f1ompt  7086  isocnv3  7310  eqfunresadj  7338  brtpos2  8214  brwitnlem  8474  brdifun  8704  omxpenlem  9047  infxpenlem  9973  ltpiord  10847  nqerf  10890  nqerid  10893  ordpinq  10903  ltxrlt  11251  ltxr  13082  trclublem  14968  oduleg  18258  oduposb  18295  join0  18371  meet0  18372  xmeterval  24327  pi1cpbl  24951  slenlt  27671  ltgov  28531  brbtwn  28833  avril1  30399  axhcompl-zf  30934  hlimadd  31129  hhcmpl  31136  hhcms  31139  hlim0  31171  fcoinvbr  32541  brprop  32627  posrasymb  32898  trleile  32904  isarchi  33143  pstmfval  33893  pstmxmet  33894  lmlim  33944  satfbrsuc  35360  brtxp  35875  brpprod  35880  brpprod3b  35882  brtxpsd2  35890  brdomain  35928  brrange  35929  brimg  35932  brapply  35933  brsuccf  35936  brrestrict  35944  brub  35949  brlb  35950  colineardim1  36056  broutsideof  36116  fneval  36347  relowlpssretop  37359  phpreu  37605  poimirlem26  37647  br1cnvres  38265  brid  38301  eqres  38329  alrmomorn  38347  brabidgaw  38354  brabidga  38355  brxrn  38363  br1cossinres  38445  br1cossxrnres  38446  brnonrel  43585  brcofffn  44027  brco2f1o  44028  brco3f1o  44029  clsneikex  44102  clsneinex  44103  clsneiel1  44104  neicvgmex  44113  neicvgel1  44115  brpermmodel  45000  climreeq  45618  xlimres  45826  xlimcl  45827  xlimclim  45829  xlimconst  45830  xlimbr  45832  xlimmnfvlem1  45837  xlimmnfvlem2  45838  xlimpnfvlem1  45841  xlimpnfvlem2  45842  xlimuni  45858  lambert0  46895  lamberte  46896  islmd  49658  iscmd  49659  lmdran  49664  cmdlan  49665  gte-lte  49717  gt-lt  49718  gte-lteh  49719  gt-lth  49720