Theorem breqi 5075

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

Syntax hints:   ↔ wb 208   = wceq 1536   class class class wbr 5069

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896  df-br 5070

This theorem is referenced by:  f1ompt  6878  isocnv3  7088  brtpos2  7901  brwitnlem  8135  brdifun  8321  omxpenlem  8621  infxpenlem  9442  ltpiord  10312  nqerf  10355  nqerid  10358  ordpinq  10368  ltxrlt  10714  ltxr  12513  trclublem  14358  oduleg  17745  oduposb  17749  meet0  17750  join0  17751  xmeterval  23045  pi1cpbl  23651  ltgov  26386  brbtwn  26688  avril1  28245  axhcompl-zf  28778  hlimadd  28973  hhcmpl  28980  hhcms  28983  hlim0  29015  fcoinvbr  30361  brprop  30436  posrasymb  30648  trleile  30657  isarchi  30815  pstmfval  31140  pstmxmet  31141  lmlim  31194  satfbrsuc  32617  eqfunresadj  33008  slenlt  33235  brtxp  33345  brpprod  33350  brpprod3b  33352  brtxpsd2  33360  brdomain  33398  brrange  33399  brimg  33402  brapply  33403  brsuccf  33406  brrestrict  33414  brub  33419  brlb  33420  colineardim1  33526  broutsideof  33586  fneval  33704  relowlpssretop  34649  phpreu  34880  poimirlem26  34922  brid  35568  eqres  35601  alrmomorn  35616  brabidgaw  35621  brabidga  35622  brxrn  35630  br1cossinres  35691  br1cossxrnres  35692  brnonrel  39955  brcofffn  40387  brco2f1o  40388  brco3f1o  40389  clsneikex  40462  clsneinex  40463  clsneiel1  40464  neicvgmex  40473  neicvgel1  40475  climreeq  41900  xlimres  42108  xlimcl  42109  xlimclim  42111  xlimconst  42112  xlimbr  42114  xlimmnfvlem1  42119  xlimmnfvlem2  42120  xlimpnfvlem1  42123  xlimpnfvlem2  42124  xlimuni  42140  gte-lte  44830  gt-lt  44831  gte-lteh  44832  gt-lth  44833