Theorem breqi 5103

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5097

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-br 5098

This theorem is referenced by:  f1ompt  7056  isocnv3  7278  eqfunresadj  7306  brtpos2  8174  brwitnlem  8434  brdifun  8666  omxpenlem  9008  infxpenlem  9925  ltpiord  10800  nqerf  10843  nqerid  10846  ordpinq  10856  ltxrlt  11205  ltxr  13031  trclublem  14920  oduleg  18215  oduposb  18252  join0  18328  meet0  18329  xmeterval  24378  pi1cpbl  25002  slenlt  27722  ltgov  28650  brbtwn  28953  avril1  30519  axhcompl-zf  31054  hlimadd  31249  hhcmpl  31256  hhcms  31259  hlim0  31291  fcoinvbr  32660  brprop  32755  posrasymb  33028  trleile  33032  isarchi  33243  pstmfval  34032  pstmxmet  34033  lmlim  34083  fineqvnttrclse  35259  satfbrsuc  35539  brtxp  36051  brpprod  36056  brpprod3b  36058  brtxpsd2  36066  brdomain  36104  brrange  36105  brimg  36108  brapply  36109  brsuccf  36113  brrestrict  36122  brub  36127  brlb  36128  colineardim1  36234  broutsideof  36294  fneval  36525  relowlpssretop  37538  phpreu  37774  poimirlem26  37816  br1cnvres  38444  brid  38482  eqres  38510  alrmomorn  38528  brabidgaw  38543  brabidga  38544  brxrn  38553  br1cossinres  38707  br1cossxrnres  38708  brnonrel  43867  brcofffn  44309  brco2f1o  44310  brco3f1o  44311  clsneikex  44384  clsneinex  44385  clsneiel1  44386  neicvgmex  44395  neicvgel1  44397  brpermmodel  45281  climreeq  45896  xlimres  46102  xlimcl  46103  xlimclim  46105  xlimconst  46106  xlimbr  46108  xlimmnfvlem1  46113  xlimmnfvlem2  46114  xlimpnfvlem1  46117  xlimpnfvlem2  46118  xlimuni  46134  lambert0  47170  lamberte  47171  islmd  49947  iscmd  49948  lmdran  49953  cmdlan  49954  gte-lte  50006  gt-lt  50007  gte-lteh  50008  gt-lth  50009