Theorem breqi 5149

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-br 5144

This theorem is referenced by:  f1ompt  7131  isocnv3  7352  eqfunresadj  7380  brtpos2  8257  brwitnlem  8545  brdifun  8775  omxpenlem  9113  infxpenlem  10053  ltpiord  10927  nqerf  10970  nqerid  10973  ordpinq  10983  ltxrlt  11331  ltxr  13157  trclublem  15034  oduleg  18335  oduposb  18374  join0  18450  meet0  18451  xmeterval  24442  pi1cpbl  25077  slenlt  27797  ltgov  28605  brbtwn  28914  avril1  30482  axhcompl-zf  31017  hlimadd  31212  hhcmpl  31219  hhcms  31222  hlim0  31254  fcoinvbr  32618  brprop  32706  posrasymb  32955  trleile  32961  isarchi  33189  pstmfval  33895  pstmxmet  33896  lmlim  33946  satfbrsuc  35371  brtxp  35881  brpprod  35886  brpprod3b  35888  brtxpsd2  35896  brdomain  35934  brrange  35935  brimg  35938  brapply  35939  brsuccf  35942  brrestrict  35950  brub  35955  brlb  35956  colineardim1  36062  broutsideof  36122  fneval  36353  relowlpssretop  37365  phpreu  37611  poimirlem26  37653  br1cnvres  38270  brid  38307  eqres  38341  alrmomorn  38359  brabidgaw  38366  brabidga  38367  brxrn  38375  br1cossinres  38448  br1cossxrnres  38449  brnonrel  43602  brcofffn  44044  brco2f1o  44045  brco3f1o  44046  clsneikex  44119  clsneinex  44120  clsneiel1  44121  neicvgmex  44130  neicvgel1  44132  climreeq  45628  xlimres  45836  xlimcl  45837  xlimclim  45839  xlimconst  45840  xlimbr  45842  xlimmnfvlem1  45847  xlimmnfvlem2  45848  xlimpnfvlem1  45851  xlimpnfvlem2  45852  xlimuni  45868  gte-lte  49243  gt-lt  49244  gte-lteh  49245  gt-lth  49246