Theorem breqi 5125

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-br 5120

This theorem is referenced by:  f1ompt  7101  isocnv3  7325  eqfunresadj  7353  brtpos2  8231  brwitnlem  8519  brdifun  8749  omxpenlem  9087  infxpenlem  10027  ltpiord  10901  nqerf  10944  nqerid  10947  ordpinq  10957  ltxrlt  11305  ltxr  13131  trclublem  15014  oduleg  18302  oduposb  18339  join0  18415  meet0  18416  xmeterval  24371  pi1cpbl  24995  slenlt  27716  ltgov  28576  brbtwn  28878  avril1  30444  axhcompl-zf  30979  hlimadd  31174  hhcmpl  31181  hhcms  31184  hlim0  31216  fcoinvbr  32586  brprop  32674  posrasymb  32945  trleile  32951  isarchi  33180  pstmfval  33927  pstmxmet  33928  lmlim  33978  satfbrsuc  35388  brtxp  35898  brpprod  35903  brpprod3b  35905  brtxpsd2  35913  brdomain  35951  brrange  35952  brimg  35955  brapply  35956  brsuccf  35959  brrestrict  35967  brub  35972  brlb  35973  colineardim1  36079  broutsideof  36139  fneval  36370  relowlpssretop  37382  phpreu  37628  poimirlem26  37670  br1cnvres  38287  brid  38324  eqres  38358  alrmomorn  38376  brabidgaw  38383  brabidga  38384  brxrn  38392  br1cossinres  38465  br1cossxrnres  38466  brnonrel  43613  brcofffn  44055  brco2f1o  44056  brco3f1o  44057  clsneikex  44130  clsneinex  44131  clsneiel1  44132  neicvgmex  44141  neicvgel1  44143  brpermmodel  45028  climreeq  45642  xlimres  45850  xlimcl  45851  xlimclim  45853  xlimconst  45854  xlimbr  45856  xlimmnfvlem1  45861  xlimmnfvlem2  45862  xlimpnfvlem1  45865  xlimpnfvlem2  45866  xlimuni  45882  lambert0  46919  lamberte  46920  islmd  49535  iscmd  49536  gte-lte  49588  gt-lt  49589  gte-lteh  49590  gt-lth  49591