Theorem breqi 5076

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

Syntax hints:   ↔ wb 205   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-br 5071

This theorem is referenced by:  f1ompt  6967  isocnv3  7183  brtpos2  8019  brwitnlem  8299  brdifun  8485  omxpenlem  8813  infxpenlem  9700  ltpiord  10574  nqerf  10617  nqerid  10620  ordpinq  10630  ltxrlt  10976  ltxr  12780  trclublem  14634  oduleg  17924  oduposb  17962  join0  18038  meet0  18039  xmeterval  23493  pi1cpbl  24113  ltgov  26862  brbtwn  27170  avril1  28728  axhcompl-zf  29261  hlimadd  29456  hhcmpl  29463  hhcms  29466  hlim0  29498  fcoinvbr  30848  brprop  30932  posrasymb  31145  trleile  31151  isarchi  31338  pstmfval  31748  pstmxmet  31749  lmlim  31799  satfbrsuc  33228  eqfunresadj  33641  slenlt  33882  brtxp  34109  brpprod  34114  brpprod3b  34116  brtxpsd2  34124  brdomain  34162  brrange  34163  brimg  34166  brapply  34167  brsuccf  34170  brrestrict  34178  brub  34183  brlb  34184  colineardim1  34290  broutsideof  34350  fneval  34468  relowlpssretop  35462  phpreu  35688  poimirlem26  35730  brid  36369  eqres  36402  alrmomorn  36417  brabidgaw  36422  brabidga  36423  brxrn  36431  br1cossinres  36492  br1cossxrnres  36493  brnonrel  41086  brcofffn  41530  brco2f1o  41531  brco3f1o  41532  clsneikex  41605  clsneinex  41606  clsneiel1  41607  neicvgmex  41616  neicvgel1  41618  climreeq  43044  xlimres  43252  xlimcl  43253  xlimclim  43255  xlimconst  43256  xlimbr  43258  xlimmnfvlem1  43263  xlimmnfvlem2  43264  xlimpnfvlem1  43267  xlimpnfvlem2  43268  xlimuni  43284  gte-lte  46312  gt-lt  46313  gte-lteh  46314  gt-lth  46315