Theorem breqi 5109

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  f1ompt  7100  isocnv3  7329  eqfunresadj  7359  brtpos2  8228  brwitnlem  8494  brdifun  8727  omxpenlem  9076  infxpenlem  10049  ltpiord  10929  nqerf  10972  nqerid  10975  ordpinq  10985  ltxrlt  11337  ltxr  13199  trclublem  15101  oduleg  18411  oduposb  18448  join0  18524  meet0  18525  xmeterval  24698  pi1cpbl  25312  lenlts  28028  ltgov  28979  brbtwn  29396  avril1  30983  axhcompl-zf  31519  hlimadd  31714  hhcmpl  31721  hhcms  31724  hlim0  31756  fcoinvbr  33118  brprop  33209  posrasymb  33447  trleile  33451  isarchi  33662  pstmfval  34447  pstmxmet  34448  lmlim  34498  morleylemrneab  35220  fineqvnttrclse  35711  satfbrsuc  36046  brtxp  36558  brpprod  36563  brpprod3b  36565  brtxpsd2  36573  brdomain  36611  brrange  36612  brimg  36615  brapply  36616  brsuccf  36620  brrestrict  36629  brub  36634  brlb  36635  colineardim1  36742  broutsideof  36802  fneval  37056  relowlpssretop  38201  phpreu  38441  poimirlem26  38478  br1cnvres  39120  brid  39158  eqres  39186  alrmomorn  39204  brabidgaw  39219  brabidga  39220  brxrn  39229  br1cossinres  39383  br1cossxrnres  39384  brnonrel  44527  brcofffn  44969  brco2f1o  44970  brco3f1o  44971  clsneikex  45044  clsneinex  45045  clsneiel1  45046  neicvgmex  45055  neicvgel1  45057  brpermmodel  45924  climreeq  46541  xlimres  46747  xlimcl  46748  xlimclim  46750  xlimconst  46751  xlimbr  46753  xlimmnfvlem1  46758  xlimmnfvlem2  46759  xlimpnfvlem1  46762  xlimpnfvlem2  46763  xlimuni  46779  lambert0  47853  lamberte  47854  islmd  50689  iscmd  50690  lmdran  50695  cmdlan  50696  gte-lte  50733  gt-lt  50734  gte-lteh  50735  gt-lth  50736