Theorem breqi 5081

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

Syntax hints:   ↔ wb 208   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-br 5076

This theorem is referenced by:  f1ompt  7056  isocnv3  7280  eqfunresadj  7308  brtpos2  8176  brwitnlem  8436  brdifun  8668  omxpenlem  9010  infxpenlem  9930  ltpiord  10805  nqerf  10848  nqerid  10851  ordpinq  10861  ltxrlt  11211  ltxr  13061  trclublem  14952  oduleg  18251  oduposb  18288  join0  18364  meet0  18365  xmeterval  24419  pi1cpbl  25033  lenlts  27738  ltgov  28687  brbtwn  28990  avril1  30555  axhcompl-zf  31091  hlimadd  31286  hhcmpl  31293  hhcms  31296  hlim0  31328  fcoinvbr  32698  brprop  32793  posrasymb  33050  trleile  33054  isarchi  33267  pstmfval  34092  pstmxmet  34093  lmlim  34143  morleylemrneab  34867  fineqvnttrclse  35320  satfbrsuc  35609  brtxp  36121  brpprod  36126  brpprod3b  36128  brtxpsd2  36136  brdomain  36174  brrange  36175  brimg  36178  brapply  36179  brsuccf  36183  brrestrict  36192  brub  36197  brlb  36198  colineardim1  36304  broutsideof  36364  fneval  36595  relowlpssretop  37741  phpreu  37986  poimirlem26  38028  br1cnvres  38656  brid  38694  eqres  38722  alrmomorn  38740  brabidgaw  38755  brabidga  38756  brxrn  38765  br1cossinres  38919  br1cossxrnres  38920  brnonrel  44048  brcofffn  44490  brco2f1o  44491  brco3f1o  44492  clsneikex  44565  clsneinex  44566  clsneiel1  44567  neicvgmex  44576  neicvgel1  44578  brpermmodel  45462  climreeq  46072  xlimres  46278  xlimcl  46279  xlimclim  46281  xlimconst  46282  xlimbr  46284  xlimmnfvlem1  46289  xlimmnfvlem2  46290  xlimpnfvlem1  46293  xlimpnfvlem2  46294  xlimuni  46310  lambert0  47364  lamberte  47365  islmd  50169  iscmd  50170  lmdran  50175  cmdlan  50176  gte-lte  50228  gt-lt  50229  gte-lteh  50230  gt-lth  50231