Theorem breqi 5153

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

Syntax hints:   ↔ wb 206   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-br 5148

This theorem is referenced by:  f1ompt  7130  isocnv3  7351  eqfunresadj  7379  brtpos2  8255  brwitnlem  8543  brdifun  8773  omxpenlem  9111  infxpenlem  10050  ltpiord  10924  nqerf  10967  nqerid  10970  ordpinq  10980  ltxrlt  11328  ltxr  13154  trclublem  15030  oduleg  18346  oduposb  18386  join0  18462  meet0  18463  xmeterval  24457  pi1cpbl  25090  slenlt  27811  ltgov  28619  brbtwn  28928  avril1  30491  axhcompl-zf  31026  hlimadd  31221  hhcmpl  31228  hhcms  31231  hlim0  31263  fcoinvbr  32624  brprop  32711  posrasymb  32939  trleile  32945  isarchi  33171  pstmfval  33856  pstmxmet  33857  lmlim  33907  satfbrsuc  35350  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  36334  relowlpssretop  37346  phpreu  37590  poimirlem26  37632  br1cnvres  38250  brid  38287  eqres  38321  alrmomorn  38339  brabidgaw  38346  brabidga  38347  brxrn  38355  br1cossinres  38428  br1cossxrnres  38429  brnonrel  43578  brcofffn  44020  brco2f1o  44021  brco3f1o  44022  clsneikex  44095  clsneinex  44096  clsneiel1  44097  neicvgmex  44106  neicvgel1  44108  climreeq  45568  xlimres  45776  xlimcl  45777  xlimclim  45779  xlimconst  45780  xlimbr  45782  xlimmnfvlem1  45787  xlimmnfvlem2  45788  xlimpnfvlem1  45791  xlimpnfvlem2  45792  xlimuni  45808  gte-lte  48954  gt-lt  48955  gte-lteh  48956  gt-lth  48957