Theorem breqi 5106

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

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

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 5101

This theorem is referenced by:  f1ompt  7067  isocnv3  7290  eqfunresadj  7318  brtpos2  8186  brwitnlem  8446  brdifun  8678  omxpenlem  9020  infxpenlem  9937  ltpiord  10812  nqerf  10855  nqerid  10858  ordpinq  10868  ltxrlt  11217  ltxr  13043  trclublem  14932  oduleg  18227  oduposb  18264  join0  18340  meet0  18341  xmeterval  24393  pi1cpbl  25017  lenlts  27737  ltgov  28687  brbtwn  28990  avril1  30556  axhcompl-zf  31092  hlimadd  31287  hhcmpl  31294  hhcms  31297  hlim0  31329  fcoinvbr  32698  brprop  32793  posrasymb  33066  trleile  33070  isarchi  33282  pstmfval  34080  pstmxmet  34081  lmlim  34131  fineqvnttrclse  35308  satfbrsuc  35588  brtxp  36100  brpprod  36105  brpprod3b  36107  brtxpsd2  36115  brdomain  36153  brrange  36154  brimg  36157  brapply  36158  brsuccf  36162  brrestrict  36171  brub  36176  brlb  36177  colineardim1  36283  broutsideof  36343  fneval  36574  relowlpssretop  37646  phpreu  37884  poimirlem26  37926  br1cnvres  38554  brid  38592  eqres  38620  alrmomorn  38638  brabidgaw  38653  brabidga  38654  brxrn  38663  br1cossinres  38817  br1cossxrnres  38818  brnonrel  43974  brcofffn  44416  brco2f1o  44417  brco3f1o  44418  clsneikex  44491  clsneinex  44492  clsneiel1  44493  neicvgmex  44502  neicvgel1  44504  brpermmodel  45388  climreeq  46002  xlimres  46208  xlimcl  46209  xlimclim  46211  xlimconst  46212  xlimbr  46214  xlimmnfvlem1  46219  xlimmnfvlem2  46220  xlimpnfvlem1  46223  xlimpnfvlem2  46224  xlimuni  46240  lambert0  47276  lamberte  47277  islmd  50053  iscmd  50054  lmdran  50059  cmdlan  50060  gte-lte  50112  gt-lt  50113  gte-lteh  50114  gt-lth  50115