Theorem breqi 5155

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

Syntax hints:   ↔ wb 205   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-br 5150

This theorem is referenced by:  f1ompt  7111  isocnv3  7329  eqfunresadj  7357  brtpos2  8217  brwitnlem  8507  brdifun  8732  omxpenlem  9073  infxpenlem  10008  ltpiord  10882  nqerf  10925  nqerid  10928  ordpinq  10938  ltxrlt  11284  ltxr  13095  trclublem  14942  oduleg  18243  oduposb  18282  join0  18358  meet0  18359  xmeterval  23938  pi1cpbl  24560  slenlt  27255  ltgov  27848  brbtwn  28157  avril1  29716  axhcompl-zf  30251  hlimadd  30446  hhcmpl  30453  hhcms  30456  hlim0  30488  fcoinvbr  31836  brprop  31919  posrasymb  32135  trleile  32141  isarchi  32328  pstmfval  32876  pstmxmet  32877  lmlim  32927  satfbrsuc  34357  brtxp  34852  brpprod  34857  brpprod3b  34859  brtxpsd2  34867  brdomain  34905  brrange  34906  brimg  34909  brapply  34910  brsuccf  34913  brrestrict  34921  brub  34926  brlb  34927  colineardim1  35033  broutsideof  35093  fneval  35237  relowlpssretop  36245  phpreu  36472  poimirlem26  36514  br1cnvres  37137  brid  37175  eqres  37209  alrmomorn  37227  brabidgaw  37234  brabidga  37235  brxrn  37244  br1cossinres  37317  br1cossxrnres  37318  brnonrel  42340  brcofffn  42782  brco2f1o  42783  brco3f1o  42784  clsneikex  42857  clsneinex  42858  clsneiel1  42859  neicvgmex  42868  neicvgel1  42870  climreeq  44329  xlimres  44537  xlimcl  44538  xlimclim  44540  xlimconst  44541  xlimbr  44543  xlimmnfvlem1  44548  xlimmnfvlem2  44549  xlimpnfvlem1  44552  xlimpnfvlem2  44553  xlimuni  44569  gte-lte  47769  gt-lt  47770  gte-lteh  47771  gt-lth  47772