Theorem breqi 5033

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

Syntax hints:   ↔ wb 209   = wceq 1542   class class class wbr 5027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811  df-br 5028

This theorem is referenced by:  f1ompt  6879  isocnv3  7092  brtpos2  7920  brwitnlem  8156  brdifun  8342  omxpenlem  8660  infxpenlem  9506  ltpiord  10380  nqerf  10423  nqerid  10426  ordpinq  10436  ltxrlt  10782  ltxr  12586  trclublem  14437  oduleg  17851  oduposb  17855  meet0  17856  join0  17857  xmeterval  23178  pi1cpbl  23789  ltgov  26535  brbtwn  26837  avril1  28392  axhcompl-zf  28925  hlimadd  29120  hhcmpl  29127  hhcms  29130  hlim0  29162  fcoinvbr  30513  brprop  30597  posrasymb  30809  trleile  30818  isarchi  31005  pstmfval  31410  pstmxmet  31411  lmlim  31461  satfbrsuc  32891  eqfunresadj  33299  slenlt  33588  brtxp  33812  brpprod  33817  brpprod3b  33819  brtxpsd2  33827  brdomain  33865  brrange  33866  brimg  33869  brapply  33870  brsuccf  33873  brrestrict  33881  brub  33886  brlb  33887  colineardim1  33993  broutsideof  34053  fneval  34171  relowlpssretop  35147  phpreu  35373  poimirlem26  35415  brid  36054  eqres  36087  alrmomorn  36102  brabidgaw  36107  brabidga  36108  brxrn  36116  br1cossinres  36177  br1cossxrnres  36178  brnonrel  40726  brcofffn  41171  brco2f1o  41172  brco3f1o  41173  clsneikex  41246  clsneinex  41247  clsneiel1  41248  neicvgmex  41257  neicvgel1  41259  climreeq  42680  xlimres  42888  xlimcl  42889  xlimclim  42891  xlimconst  42892  xlimbr  42894  xlimmnfvlem1  42899  xlimmnfvlem2  42900  xlimpnfvlem1  42903  xlimpnfvlem2  42904  xlimuni  42920  gte-lte  45863  gt-lt  45864  gte-lteh  45865  gt-lth  45866