Theorem breqi 4659

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

Syntax hints:   ↔ wb 196   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-br 4654

This theorem is referenced by:  f1ompt  6382  isocnv3  6582  brtpos2  7358  brwitnlem  7587  brdifun  7771  omxpenlem  8061  infxpenlem  8836  ltpiord  9709  nqerf  9752  nqerid  9755  ordpinq  9765  ltxrlt  10108  ltxr  11949  trclublem  13734  oduleg  17132  oduposb  17136  meet0  17137  join0  17138  xmeterval  22237  pi1cpbl  22844  ltgov  25492  brbtwn  25779  rgrprop  26456  rusgrprop  26458  avril1  27319  axhcompl-zf  27855  hlimadd  28050  hhcmpl  28057  hhcms  28060  hlim0  28092  fcoinvbr  29419  posrasymb  29657  trleile  29666  isarchi  29736  pstmfval  29939  pstmxmet  29940  lmlim  29993  eqfunresadj  31659  slenlt  31877  brtxp  31987  brpprod  31992  brpprod3b  31994  brtxpsd2  32002  brdomain  32040  brrange  32041  brimg  32044  brapply  32045  brsuccf  32048  brrestrict  32056  brub  32061  brlb  32062  colineardim1  32168  broutsideof  32228  fneval  32347  relowlpssretop  33212  phpreu  33393  poimirlem26  33435  brid  34077  eqres  34108  alrmomo  34123  bropabid  34128  brnonrel  37895  brcofffn  38329  brco2f1o  38330  brco3f1o  38331  clsneikex  38404  clsneinex  38405  clsneiel1  38406  neicvgmex  38415  neicvgel1  38417  climreeq  39845  xlimres  40047  xlimcl  40048  xlimclim  40050  xlimconst  40051  xlimbr  40053  xlimmnfvlem1  40058  xlimmnfvlem2  40059  xlimpnfvlem1  40062  xlimpnfvlem2  40063  gte-lte  42465  gt-lt  42466  gte-lteh  42467  gt-lth  42468