Theorem breqi 5092

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-br 5087

This theorem is referenced by:  f1ompt  7061  isocnv3  7284  eqfunresadj  7312  brtpos2  8179  brwitnlem  8439  brdifun  8671  omxpenlem  9013  infxpenlem  9932  ltpiord  10807  nqerf  10850  nqerid  10853  ordpinq  10863  ltxrlt  11213  ltxr  13063  trclublem  14954  oduleg  18253  oduposb  18290  join0  18366  meet0  18367  xmeterval  24413  pi1cpbl  25027  lenlts  27736  ltgov  28685  brbtwn  28988  avril1  30554  axhcompl-zf  31090  hlimadd  31285  hhcmpl  31292  hhcms  31295  hlim0  31327  fcoinvbr  32696  brprop  32791  posrasymb  33048  trleile  33052  isarchi  33264  pstmfval  34062  pstmxmet  34063  lmlim  34113  fineqvnttrclse  35290  satfbrsuc  35570  brtxp  36082  brpprod  36087  brpprod3b  36089  brtxpsd2  36097  brdomain  36135  brrange  36136  brimg  36139  brapply  36140  brsuccf  36144  brrestrict  36153  brub  36158  brlb  36159  colineardim1  36265  broutsideof  36325  fneval  36556  relowlpssretop  37702  phpreu  37947  poimirlem26  37989  br1cnvres  38617  brid  38655  eqres  38683  alrmomorn  38701  brabidgaw  38716  brabidga  38717  brxrn  38726  br1cossinres  38880  br1cossxrnres  38881  brnonrel  44042  brcofffn  44484  brco2f1o  44485  brco3f1o  44486  clsneikex  44559  clsneinex  44560  clsneiel1  44561  neicvgmex  44570  neicvgel1  44572  brpermmodel  45456  climreeq  46069  xlimres  46275  xlimcl  46276  xlimclim  46278  xlimconst  46279  xlimbr  46281  xlimmnfvlem1  46286  xlimmnfvlem2  46287  xlimpnfvlem1  46290  xlimpnfvlem2  46291  xlimuni  46307  lambert0  47355  lamberte  47356  islmd  50160  iscmd  50161  lmdran  50166  cmdlan  50167  gte-lte  50219  gt-lt  50220  gte-lteh  50221  gt-lth  50222