Theorem breqi 5120

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

Syntax hints:   ↔ wb 209   = wceq 1568   class class class wbr 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2762  df-clel 2845  df-br 5115

This theorem is referenced by:  f1ompt  7110  isocnv3  7334  eqfunresadj  7362  brtpos2  8231  brwitnlem  8495  brdifun  8728  omxpenlem  9069  infxpenlem  10000  ltpiord  10875  nqerf  10918  nqerid  10921  ordpinq  10931  ltxrlt  11283  ltxr  13143  trclublem  15035  oduleg  18349  oduposb  18386  join0  18462  meet0  18463  xmeterval  24572  pi1cpbl  25186  lenlts  27896  ltgov  28846  brbtwn  29219  avril1  30784  axhcompl-zf  31320  hlimadd  31515  hhcmpl  31522  hhcms  31525  hlim0  31557  fcoinvbr  32920  brprop  33012  posrasymb  33257  trleile  33261  isarchi  33472  pstmfval  34256  pstmxmet  34257  lmlim  34307  morleylemrneab  35028  fineqvnttrclse  35495  satfbrsuc  35816  brtxp  36328  brpprod  36333  brpprod3b  36335  brtxpsd2  36343  brdomain  36381  brrange  36382  brimg  36385  brapply  36386  brsuccf  36390  brrestrict  36399  brub  36404  brlb  36405  colineardim1  36511  broutsideof  36571  fneval  36811  relowlpssretop  37958  phpreu  38203  poimirlem26  38245  br1cnvres  38873  brid  38911  eqres  38939  alrmomorn  38957  brabidgaw  38972  brabidga  38973  brxrn  38982  br1cossinres  39136  br1cossxrnres  39137  brnonrel  44267  brcofffn  44709  brco2f1o  44710  brco3f1o  44711  clsneikex  44784  clsneinex  44785  clsneiel1  44786  neicvgmex  44795  neicvgel1  44797  brpermmodel  45664  climreeq  46281  xlimres  46487  xlimcl  46488  xlimclim  46490  xlimconst  46491  xlimbr  46493  xlimmnfvlem1  46498  xlimmnfvlem2  46499  xlimpnfvlem1  46502  xlimpnfvlem2  46503  xlimuni  46519  lambert0  47573  lamberte  47574  islmd  50392  iscmd  50393  lmdran  50398  cmdlan  50399  gte-lte  50451  gt-lt  50452  gte-lteh  50453  gt-lth  50454