Theorem breqi 5114

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837  df-br 5109

This theorem is used by:  f1ompt  7106  isocnv3  7330  eqfunresadj  7360  brtpos2  8226  brwitnlem  8490  brdifun  8723  omxpenlem  9064  infxpenlem  10004  ltpiord  10878  nqerf  10921  nqerid  10924  ordpinq  10934  ltxrlt  11286  ltxr  13146  trclublem  15039  oduleg  18352  oduposb  18389  join0  18465  meet0  18466  xmeterval  24600  pi1cpbl  25214  lenlts  27927  ltgov  28877  brbtwn  29260  avril1  30825  axhcompl-zf  31361  hlimadd  31556  hhcmpl  31563  hhcms  31566  hlim0  31598  fcoinvbr  32961  brprop  33053  posrasymb  33296  trleile  33300  isarchi  33511  pstmfval  34295  pstmxmet  34296  lmlim  34346  morleylemrneab  35067  fineqvnttrclse  35545  satfbrsuc  35866  brtxp  36378  brpprod  36383  brpprod3b  36385  brtxpsd2  36393  brdomain  36431  brrange  36432  brimg  36435  brapply  36436  brsuccf  36440  brrestrict  36449  brub  36454  brlb  36455  colineardim1  36561  broutsideof  36621  fneval  36891  relowlpssretop  38038  phpreu  38283  poimirlem26  38325  br1cnvres  38951  brid  38989  eqres  39017  alrmomorn  39035  brabidgaw  39050  brabidga  39051  brxrn  39060  br1cossinres  39214  br1cossxrnres  39215  brnonrel  44343  brcofffn  44785  brco2f1o  44786  brco3f1o  44787  clsneikex  44860  clsneinex  44861  clsneiel1  44862  neicvgmex  44871  neicvgel1  44873  brpermmodel  45740  climreeq  46357  xlimres  46563  xlimcl  46564  xlimclim  46566  xlimconst  46567  xlimbr  46569  xlimmnfvlem1  46574  xlimmnfvlem2  46575  xlimpnfvlem1  46578  xlimpnfvlem2  46579  xlimuni  46595  lambert0  47652  lamberte  47653  islmd  50471  iscmd  50472  lmdran  50477  cmdlan  50478  gte-lte  50530  gt-lt  50531  gte-lteh  50532  gt-lth  50533