Theorem breqi 5105

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-br 5100

This theorem is referenced by:  f1ompt  7058  isocnv3  7280  eqfunresadj  7308  brtpos2  8176  brwitnlem  8436  brdifun  8668  omxpenlem  9010  infxpenlem  9927  ltpiord  10802  nqerf  10845  nqerid  10848  ordpinq  10858  ltxrlt  11207  ltxr  13033  trclublem  14922  oduleg  18217  oduposb  18254  join0  18330  meet0  18331  xmeterval  24380  pi1cpbl  25004  lenlts  27724  ltgov  28673  brbtwn  28976  avril1  30542  axhcompl-zf  31077  hlimadd  31272  hhcmpl  31279  hhcms  31282  hlim0  31314  fcoinvbr  32683  brprop  32778  posrasymb  33051  trleile  33055  isarchi  33266  pstmfval  34055  pstmxmet  34056  lmlim  34106  fineqvnttrclse  35282  satfbrsuc  35562  brtxp  36074  brpprod  36079  brpprod3b  36081  brtxpsd2  36089  brdomain  36127  brrange  36128  brimg  36131  brapply  36132  brsuccf  36136  brrestrict  36145  brub  36150  brlb  36151  colineardim1  36257  broutsideof  36317  fneval  36548  relowlpssretop  37571  phpreu  37807  poimirlem26  37849  br1cnvres  38477  brid  38515  eqres  38543  alrmomorn  38561  brabidgaw  38576  brabidga  38577  brxrn  38586  br1cossinres  38740  br1cossxrnres  38741  brnonrel  43897  brcofffn  44339  brco2f1o  44340  brco3f1o  44341  clsneikex  44414  clsneinex  44415  clsneiel1  44416  neicvgmex  44425  neicvgel1  44427  brpermmodel  45311  climreeq  45926  xlimres  46132  xlimcl  46133  xlimclim  46135  xlimconst  46136  xlimbr  46138  xlimmnfvlem1  46143  xlimmnfvlem2  46144  xlimpnfvlem1  46147  xlimpnfvlem2  46148  xlimuni  46164  lambert0  47200  lamberte  47201  islmd  49977  iscmd  49978  lmdran  49983  cmdlan  49984  gte-lte  50036  gt-lt  50037  gte-lteh  50038  gt-lth  50039