Theorem breqi 5113

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

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

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 5108

This theorem is referenced by:  f1ompt  7083  isocnv3  7307  eqfunresadj  7335  brtpos2  8211  brwitnlem  8471  brdifun  8701  omxpenlem  9042  infxpenlem  9966  ltpiord  10840  nqerf  10883  nqerid  10886  ordpinq  10896  ltxrlt  11244  ltxr  13075  trclublem  14961  oduleg  18251  oduposb  18288  join0  18364  meet0  18365  xmeterval  24320  pi1cpbl  24944  slenlt  27664  ltgov  28524  brbtwn  28826  avril1  30392  axhcompl-zf  30927  hlimadd  31122  hhcmpl  31129  hhcms  31132  hlim0  31164  fcoinvbr  32534  brprop  32620  posrasymb  32891  trleile  32897  isarchi  33136  pstmfval  33886  pstmxmet  33887  lmlim  33937  satfbrsuc  35353  brtxp  35868  brpprod  35873  brpprod3b  35875  brtxpsd2  35883  brdomain  35921  brrange  35922  brimg  35925  brapply  35926  brsuccf  35929  brrestrict  35937  brub  35942  brlb  35943  colineardim1  36049  broutsideof  36109  fneval  36340  relowlpssretop  37352  phpreu  37598  poimirlem26  37640  br1cnvres  38258  brid  38294  eqres  38322  alrmomorn  38340  brabidgaw  38347  brabidga  38348  brxrn  38356  br1cossinres  38438  br1cossxrnres  38439  brnonrel  43578  brcofffn  44020  brco2f1o  44021  brco3f1o  44022  clsneikex  44095  clsneinex  44096  clsneiel1  44097  neicvgmex  44106  neicvgel1  44108  brpermmodel  44993  climreeq  45611  xlimres  45819  xlimcl  45820  xlimclim  45822  xlimconst  45823  xlimbr  45825  xlimmnfvlem1  45830  xlimmnfvlem2  45831  xlimpnfvlem1  45834  xlimpnfvlem2  45835  xlimuni  45851  lambert0  46888  lamberte  46889  islmd  49654  iscmd  49655  lmdran  49660  cmdlan  49661  gte-lte  49713  gt-lt  49714  gte-lteh  49715  gt-lth  49716