Theorem breqi 5108

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-br 5103

This theorem is used by:  f1ompt  7111  isocnv3  7340  eqfunresadj  7370  brtpos2  8249  brwitnlem  8515  brdifun  8748  omxpenlem  9097  infxpenlem  10092  ltpiord  10972  nqerf  11015  nqerid  11018  ordpinq  11028  ltxrlt  11380  ltxr  13244  trclublem  15148  oduleg  18464  oduposb  18501  join0  18577  meet0  18578  xmeterval  24751  pi1cpbl  25365  lenlts  28109  ltgov  29060  brbtwn  29477  avril1  31064  axhcompl-zf  31600  hlimadd  31795  hhcmpl  31802  hhcms  31805  hlim0  31837  fcoinvbr  33199  brprop  33290  posrasymb  33528  trleile  33532  isarchi  33743  pstmfval  34528  pstmxmet  34529  lmlim  34579  morleylemrneab  35300  fineqvnttrclse  35792  satfbrsuc  36131  brtxp  36642  brpprod  36647  brpprod3b  36649  brtxpsd2  36657  brdomain  36695  brrange  36696  brimg  36699  brapply  36700  brsuccf  36704  brrestrict  36713  brub  36718  brlb  36719  colineardim1  36826  broutsideof  36886  fneval  37140  relowlpssretop  38288  phpreu  38528  poimirlem26  38565  br1cnvres  39207  brid  39245  eqres  39273  alrmomorn  39291  brabidgaw  39306  brabidga  39307  brxrn  39316  br1cossinres  39470  br1cossxrnres  39471  brnonrel  44589  brcofffn  45031  brco2f1o  45032  brco3f1o  45033  clsneikex  45106  clsneinex  45107  clsneiel1  45108  neicvgmex  45117  neicvgel1  45119  brpermmodel  45993  climreeq  46625  xlimres  46831  xlimcl  46832  xlimclim  46834  xlimconst  46835  xlimbr  46837  xlimmnfvlem1  46842  xlimmnfvlem2  46843  xlimpnfvlem1  46846  xlimpnfvlem2  46847  xlimuni  46863  lambert0  47937  lamberte  47938  islmd  50773  iscmd  50774  lmdran  50779  cmdlan  50780  gte-lte  50817  gt-lt  50818  gte-lteh  50819  gt-lth  50820