Theorem breqi 5108

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5103

This theorem is referenced by:  f1ompt  7065  isocnv3  7289  eqfunresadj  7317  brtpos2  8188  brwitnlem  8448  brdifun  8678  omxpenlem  9019  infxpenlem  9944  ltpiord  10818  nqerf  10861  nqerid  10864  ordpinq  10874  ltxrlt  11222  ltxr  13053  trclublem  14938  oduleg  18232  oduposb  18269  join0  18345  meet0  18346  xmeterval  24354  pi1cpbl  24978  slenlt  27698  ltgov  28578  brbtwn  28880  avril1  30443  axhcompl-zf  30978  hlimadd  31173  hhcmpl  31180  hhcms  31183  hlim0  31215  fcoinvbr  32585  brprop  32671  posrasymb  32940  trleile  32944  isarchi  33152  pstmfval  33880  pstmxmet  33881  lmlim  33931  satfbrsuc  35347  brtxp  35862  brpprod  35867  brpprod3b  35869  brtxpsd2  35877  brdomain  35915  brrange  35916  brimg  35919  brapply  35920  brsuccf  35923  brrestrict  35931  brub  35936  brlb  35937  colineardim1  36043  broutsideof  36103  fneval  36334  relowlpssretop  37346  phpreu  37592  poimirlem26  37634  br1cnvres  38252  brid  38288  eqres  38316  alrmomorn  38334  brabidgaw  38341  brabidga  38342  brxrn  38350  br1cossinres  38432  br1cossxrnres  38433  brnonrel  43572  brcofffn  44014  brco2f1o  44015  brco3f1o  44016  clsneikex  44089  clsneinex  44090  clsneiel1  44091  neicvgmex  44100  neicvgel1  44102  brpermmodel  44987  climreeq  45605  xlimres  45813  xlimcl  45814  xlimclim  45816  xlimconst  45817  xlimbr  45819  xlimmnfvlem1  45824  xlimmnfvlem2  45825  xlimpnfvlem1  45828  xlimpnfvlem2  45829  xlimuni  45845  lambert0  46882  lamberte  46883  islmd  49648  iscmd  49649  lmdran  49654  cmdlan  49655  gte-lte  49707  gt-lt  49708  gte-lteh  49709  gt-lth  49710