Theorem breqi 5108

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5102

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5103

This theorem is referenced by:  f1ompt  7065  isocnv3  7289  eqfunresadj  7317  brtpos2  8188  brwitnlem  8448  brdifun  8678  omxpenlem  9019  infxpenlem  9942  ltpiord  10816  nqerf  10859  nqerid  10862  ordpinq  10872  ltxrlt  11220  ltxr  13051  trclublem  14937  oduleg  18231  oduposb  18268  join0  18344  meet0  18345  xmeterval  24353  pi1cpbl  24977  slenlt  27697  ltgov  28577  brbtwn  28879  avril1  30442  axhcompl-zf  30977  hlimadd  31172  hhcmpl  31179  hhcms  31182  hlim0  31214  fcoinvbr  32584  brprop  32670  posrasymb  32939  trleile  32943  isarchi  33151  pstmfval  33879  pstmxmet  33880  lmlim  33930  satfbrsuc  35346  brtxp  35861  brpprod  35866  brpprod3b  35868  brtxpsd2  35876  brdomain  35914  brrange  35915  brimg  35918  brapply  35919  brsuccf  35922  brrestrict  35930  brub  35935  brlb  35936  colineardim1  36042  broutsideof  36102  fneval  36333  relowlpssretop  37345  phpreu  37591  poimirlem26  37633  br1cnvres  38251  brid  38287  eqres  38315  alrmomorn  38333  brabidgaw  38340  brabidga  38341  brxrn  38349  br1cossinres  38431  br1cossxrnres  38432  brnonrel  43571  brcofffn  44013  brco2f1o  44014  brco3f1o  44015  clsneikex  44088  clsneinex  44089  clsneiel1  44090  neicvgmex  44099  neicvgel1  44101  brpermmodel  44986  climreeq  45604  xlimres  45812  xlimcl  45813  xlimclim  45815  xlimconst  45816  xlimbr  45818  xlimmnfvlem1  45823  xlimmnfvlem2  45824  xlimpnfvlem1  45827  xlimpnfvlem2  45828  xlimuni  45844  lambert0  46881  lamberte  46882  islmd  49647  iscmd  49648  lmdran  49653  cmdlan  49654  gte-lte  49706  gt-lt  49707  gte-lteh  49708  gt-lth  49709