Theorem breqi 5098

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

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

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 5093

This theorem is referenced by:  f1ompt  7045  isocnv3  7269  eqfunresadj  7297  brtpos2  8165  brwitnlem  8425  brdifun  8655  omxpenlem  8995  infxpenlem  9907  ltpiord  10781  nqerf  10824  nqerid  10827  ordpinq  10837  ltxrlt  11186  ltxr  13017  trclublem  14902  oduleg  18196  oduposb  18233  join0  18309  meet0  18310  xmeterval  24318  pi1cpbl  24942  slenlt  27662  ltgov  28546  brbtwn  28848  avril1  30411  axhcompl-zf  30946  hlimadd  31141  hhcmpl  31148  hhcms  31151  hlim0  31183  fcoinvbr  32554  brprop  32647  posrasymb  32918  trleile  32922  isarchi  33133  pstmfval  33879  pstmxmet  33880  lmlim  33930  fineqvnttrclse  35093  satfbrsuc  35359  brtxp  35874  brpprod  35879  brpprod3b  35881  brtxpsd2  35889  brdomain  35927  brrange  35928  brimg  35931  brapply  35932  brsuccf  35935  brrestrict  35943  brub  35948  brlb  35949  colineardim1  36055  broutsideof  36115  fneval  36346  relowlpssretop  37358  phpreu  37604  poimirlem26  37646  br1cnvres  38264  brid  38300  eqres  38328  alrmomorn  38346  brabidgaw  38353  brabidga  38354  brxrn  38362  br1cossinres  38444  br1cossxrnres  38445  brnonrel  43582  brcofffn  44024  brco2f1o  44025  brco3f1o  44026  clsneikex  44099  clsneinex  44100  clsneiel1  44101  neicvgmex  44110  neicvgel1  44112  brpermmodel  44997  climreeq  45614  xlimres  45822  xlimcl  45823  xlimclim  45825  xlimconst  45826  xlimbr  45828  xlimmnfvlem1  45833  xlimmnfvlem2  45834  xlimpnfvlem1  45837  xlimpnfvlem2  45838  xlimuni  45854  lambert0  46891  lamberte  46892  islmd  49670  iscmd  49671  lmdran  49676  cmdlan  49677  gte-lte  49729  gt-lt  49730  gte-lteh  49731  gt-lth  49732