Theorem breqi 5154

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

Syntax hints:   ↔ wb 205   = wceq 1540   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809  df-br 5149

This theorem is referenced by:  f1ompt  7112  isocnv3  7332  eqfunresadj  7360  brtpos2  8223  brwitnlem  8513  brdifun  8738  omxpenlem  9079  infxpenlem  10014  ltpiord  10888  nqerf  10931  nqerid  10934  ordpinq  10944  ltxrlt  11291  ltxr  13102  trclublem  14949  oduleg  18250  oduposb  18289  join0  18365  meet0  18366  xmeterval  24171  pi1cpbl  24804  slenlt  27506  ltgov  28130  brbtwn  28439  avril1  29998  axhcompl-zf  30533  hlimadd  30728  hhcmpl  30735  hhcms  30738  hlim0  30770  fcoinvbr  32118  brprop  32201  posrasymb  32417  trleile  32423  isarchi  32613  pstmfval  33189  pstmxmet  33190  lmlim  33240  satfbrsuc  34670  brtxp  35171  brpprod  35176  brpprod3b  35178  brtxpsd2  35186  brdomain  35224  brrange  35225  brimg  35228  brapply  35229  brsuccf  35232  brrestrict  35240  brub  35245  brlb  35246  colineardim1  35352  broutsideof  35412  fneval  35553  relowlpssretop  36561  phpreu  36788  poimirlem26  36830  br1cnvres  37453  brid  37491  eqres  37525  alrmomorn  37543  brabidgaw  37550  brabidga  37551  brxrn  37560  br1cossinres  37633  br1cossxrnres  37634  brnonrel  42655  brcofffn  43097  brco2f1o  43098  brco3f1o  43099  clsneikex  43172  clsneinex  43173  clsneiel1  43174  neicvgmex  43183  neicvgel1  43185  climreeq  44640  xlimres  44848  xlimcl  44849  xlimclim  44851  xlimconst  44852  xlimbr  44854  xlimmnfvlem1  44859  xlimmnfvlem2  44860  xlimpnfvlem1  44863  xlimpnfvlem2  44864  xlimuni  44880  gte-lte  47869  gt-lt  47870  gte-lteh  47871  gt-lth  47872