Theorem breqi 5095

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

Syntax hints:   ↔ wb 206   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-br 5090

This theorem is referenced by:  f1ompt  7044  isocnv3  7266  eqfunresadj  7294  brtpos2  8162  brwitnlem  8422  brdifun  8652  omxpenlem  8991  infxpenlem  9904  ltpiord  10778  nqerf  10821  nqerid  10824  ordpinq  10834  ltxrlt  11183  ltxr  13014  trclublem  14902  oduleg  18196  oduposb  18233  join0  18309  meet0  18310  xmeterval  24347  pi1cpbl  24971  slenlt  27691  ltgov  28575  brbtwn  28877  avril1  30443  axhcompl-zf  30978  hlimadd  31173  hhcmpl  31180  hhcms  31183  hlim0  31215  fcoinvbr  32585  brprop  32678  posrasymb  32948  trleile  32952  isarchi  33151  pstmfval  33909  pstmxmet  33910  lmlim  33960  fineqvnttrclse  35144  satfbrsuc  35410  brtxp  35922  brpprod  35927  brpprod3b  35929  brtxpsd2  35937  brdomain  35975  brrange  35976  brimg  35979  brapply  35980  brsuccf  35984  brrestrict  35993  brub  35998  brlb  35999  colineardim1  36105  broutsideof  36165  fneval  36396  relowlpssretop  37408  phpreu  37643  poimirlem26  37685  br1cnvres  38305  brid  38343  eqres  38371  alrmomorn  38389  brabidgaw  38396  brabidga  38397  brxrn  38406  br1cossinres  38548  br1cossxrnres  38549  brnonrel  43681  brcofffn  44123  brco2f1o  44124  brco3f1o  44125  clsneikex  44198  clsneinex  44199  clsneiel1  44200  neicvgmex  44209  neicvgel1  44211  brpermmodel  45095  climreeq  45712  xlimres  45918  xlimcl  45919  xlimclim  45921  xlimconst  45922  xlimbr  45924  xlimmnfvlem1  45929  xlimmnfvlem2  45930  xlimpnfvlem1  45933  xlimpnfvlem2  45934  xlimuni  45950  lambert0  46986  lamberte  46987  islmd  49765  iscmd  49766  lmdran  49771  cmdlan  49772  gte-lte  49824  gt-lt  49825  gte-lteh  49826  gt-lth  49827