Theorem breqi 4968

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

Syntax hints:   ↔ wb 207   = wceq 1522   class class class wbr 4962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863  df-br 4963

This theorem is referenced by:  f1ompt  6738  isocnv3  6948  brtpos2  7749  brwitnlem  7983  brdifun  8168  omxpenlem  8465  infxpenlem  9285  ltpiord  10155  nqerf  10198  nqerid  10201  ordpinq  10211  ltxrlt  10558  ltxr  12360  trclublem  14189  oduleg  17571  oduposb  17575  meet0  17576  join0  17577  xmeterval  22725  pi1cpbl  23331  ltgov  26065  brbtwn  26368  avril1  27933  axhcompl-zf  28466  hlimadd  28661  hhcmpl  28668  hhcms  28671  hlim0  28703  fcoinvbr  30048  brprop  30121  posrasymb  30318  trleile  30327  isarchi  30449  pstmfval  30753  pstmxmet  30754  lmlim  30807  satfbrsuc  32221  eqfunresadj  32612  slenlt  32840  brtxp  32950  brpprod  32955  brpprod3b  32957  brtxpsd2  32965  brdomain  33003  brrange  33004  brimg  33007  brapply  33008  brsuccf  33011  brrestrict  33019  brub  33024  brlb  33025  colineardim1  33131  broutsideof  33191  fneval  33309  relowlpssretop  34176  phpreu  34407  poimirlem26  34449  brid  35096  eqres  35129  alrmomorn  35144  brabidga  35149  brxrn  35157  br1cossinres  35218  br1cossxrnres  35219  brnonrel  39434  brcofffn  39866  brco2f1o  39867  brco3f1o  39868  clsneikex  39941  clsneinex  39942  clsneiel1  39943  neicvgmex  39952  neicvgel1  39954  climreeq  41436  xlimres  41644  xlimcl  41645  xlimclim  41647  xlimconst  41648  xlimbr  41650  xlimmnfvlem1  41655  xlimmnfvlem2  41656  xlimpnfvlem1  41659  xlimpnfvlem2  41660  xlimuni  41676  gte-lte  44303  gt-lt  44304  gte-lteh  44305  gt-lth  44306