Theorem breqi 5074

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

Syntax hints:   ↔ wb 208   = wceq 1537   class class class wbr 5068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-br 5069

This theorem is referenced by:  f1ompt  6877  isocnv3  7087  brtpos2  7900  brwitnlem  8134  brdifun  8320  omxpenlem  8620  infxpenlem  9441  ltpiord  10311  nqerf  10354  nqerid  10357  ordpinq  10367  ltxrlt  10713  ltxr  12513  trclublem  14357  oduleg  17744  oduposb  17748  meet0  17749  join0  17750  xmeterval  23044  pi1cpbl  23650  ltgov  26385  brbtwn  26687  avril1  28244  axhcompl-zf  28777  hlimadd  28972  hhcmpl  28979  hhcms  28982  hlim0  29014  fcoinvbr  30360  brprop  30435  posrasymb  30646  trleile  30655  isarchi  30813  pstmfval  31138  pstmxmet  31139  lmlim  31192  satfbrsuc  32615  eqfunresadj  33006  slenlt  33233  brtxp  33343  brpprod  33348  brpprod3b  33350  brtxpsd2  33358  brdomain  33396  brrange  33397  brimg  33400  brapply  33401  brsuccf  33404  brrestrict  33412  brub  33417  brlb  33418  colineardim1  33524  broutsideof  33584  fneval  33702  relowlpssretop  34647  phpreu  34878  poimirlem26  34920  brid  35566  eqres  35599  alrmomorn  35614  brabidgaw  35619  brabidga  35620  brxrn  35628  br1cossinres  35689  br1cossxrnres  35690  brnonrel  39956  brcofffn  40388  brco2f1o  40389  brco3f1o  40390  clsneikex  40463  clsneinex  40464  clsneiel1  40465  neicvgmex  40474  neicvgel1  40476  climreeq  41901  xlimres  42109  xlimcl  42110  xlimclim  42112  xlimconst  42113  xlimbr  42115  xlimmnfvlem1  42120  xlimmnfvlem2  42121  xlimpnfvlem1  42124  xlimpnfvlem2  42125  xlimuni  42141  gte-lte  44830  gt-lt  44831  gte-lteh  44832  gt-lth  44833