Theorem breqi 5091

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-br 5086

This theorem is referenced by:  f1ompt  7063  isocnv3  7287  eqfunresadj  7315  brtpos2  8182  brwitnlem  8442  brdifun  8674  omxpenlem  9016  infxpenlem  9935  ltpiord  10810  nqerf  10853  nqerid  10856  ordpinq  10866  ltxrlt  11216  ltxr  13066  trclublem  14957  oduleg  18256  oduposb  18293  join0  18369  meet0  18370  xmeterval  24397  pi1cpbl  25011  lenlts  27716  ltgov  28665  brbtwn  28968  avril1  30533  axhcompl-zf  31069  hlimadd  31264  hhcmpl  31271  hhcms  31274  hlim0  31306  fcoinvbr  32675  brprop  32770  posrasymb  33027  trleile  33031  isarchi  33243  pstmfval  34040  pstmxmet  34041  lmlim  34091  fineqvnttrclse  35268  satfbrsuc  35548  brtxp  36060  brpprod  36065  brpprod3b  36067  brtxpsd2  36075  brdomain  36113  brrange  36114  brimg  36117  brapply  36118  brsuccf  36122  brrestrict  36131  brub  36136  brlb  36137  colineardim1  36243  broutsideof  36303  fneval  36534  relowlpssretop  37680  phpreu  37925  poimirlem26  37967  br1cnvres  38595  brid  38633  eqres  38661  alrmomorn  38679  brabidgaw  38694  brabidga  38695  brxrn  38704  br1cossinres  38858  br1cossxrnres  38859  brnonrel  44016  brcofffn  44458  brco2f1o  44459  brco3f1o  44460  clsneikex  44533  clsneinex  44534  clsneiel1  44535  neicvgmex  44544  neicvgel1  44546  brpermmodel  45430  climreeq  46043  xlimres  46249  xlimcl  46250  xlimclim  46252  xlimconst  46253  xlimbr  46255  xlimmnfvlem1  46260  xlimmnfvlem2  46261  xlimpnfvlem1  46264  xlimpnfvlem2  46265  xlimuni  46281  lambert0  47335  lamberte  47336  islmd  50140  iscmd  50141  lmdran  50146  cmdlan  50147  gte-lte  50199  gt-lt  50200  gte-lteh  50201  gt-lth  50202