Theorem breqi 5113

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-br 5108

This theorem is used by:  f1ompt  7107  isocnv3  7336  eqfunresadj  7366  brtpos2  8233  brwitnlem  8497  brdifun  8730  omxpenlem  9079  infxpenlem  10019  ltpiord  10899  nqerf  10942  nqerid  10945  ordpinq  10955  ltxrlt  11307  ltxr  13168  trclublem  15070  oduleg  18382  oduposb  18419  join0  18495  meet0  18496  xmeterval  24659  pi1cpbl  25273  lenlts  27986  ltgov  28937  brbtwn  29342  avril1  30929  axhcompl-zf  31465  hlimadd  31660  hhcmpl  31667  hhcms  31670  hlim0  31702  fcoinvbr  33065  brprop  33156  posrasymb  33394  trleile  33398  isarchi  33609  pstmfval  34393  pstmxmet  34394  lmlim  34444  morleylemrneab  35166  fineqvnttrclse  35637  satfbrsuc  35932  brtxp  36444  brpprod  36449  brpprod3b  36451  brtxpsd2  36459  brdomain  36497  brrange  36498  brimg  36501  brapply  36502  brsuccf  36506  brrestrict  36515  brub  36520  brlb  36521  colineardim1  36628  broutsideof  36688  fneval  36958  relowlpssretop  38105  phpreu  38345  poimirlem26  38382  br1cnvres  39009  brid  39047  eqres  39075  alrmomorn  39093  brabidgaw  39108  brabidga  39109  brxrn  39118  br1cossinres  39272  br1cossxrnres  39273  brnonrel  44416  brcofffn  44858  brco2f1o  44859  brco3f1o  44860  clsneikex  44933  clsneinex  44934  clsneiel1  44935  neicvgmex  44944  neicvgel1  44946  brpermmodel  45813  climreeq  46430  xlimres  46636  xlimcl  46637  xlimclim  46639  xlimconst  46640  xlimbr  46642  xlimmnfvlem1  46647  xlimmnfvlem2  46648  xlimpnfvlem1  46651  xlimpnfvlem2  46652  xlimuni  46668  lambert0  47742  lamberte  47743  islmd  50578  iscmd  50579  lmdran  50584  cmdlan  50585  gte-lte  50637  gt-lt  50638  gte-lteh  50639  gt-lth  50640