Theorem breqi 4589

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

Syntax hints:   ↔ wb 195   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-br 4584

This theorem is referenced by:  f1ompt  6290  isocnv3  6482  brtpos2  7245  brwitnlem  7474  brdifun  7658  omxpenlem  7946  infxpenlem  8719  ltpiord  9588  nqerf  9631  nqerid  9634  ordpinq  9644  ltxrlt  9987  ltxr  11825  trclublem  13582  oduleg  16955  oduposb  16959  meet0  16960  join0  16961  xmeterval  22047  pi1cpbl  22652  ltgov  25292  brbtwn  25579  rgraprop  26455  rusgraprop  26456  rusgrargra  26457  avril1  26711  axhcompl-zf  27239  hlimadd  27434  hhcmpl  27441  hhcms  27444  hlim0  27476  fcoinvbr  28799  posrasymb  28988  trleile  28997  isarchi  29067  pstmfval  29267  pstmxmet  29268  lmlim  29321  brtxp  31157  brpprod  31162  brpprod3b  31164  brtxpsd2  31172  brdomain  31210  brrange  31211  brimg  31214  brapply  31215  brsuccf  31218  brrestrict  31226  brub  31231  brlb  31232  colineardim1  31338  broutsideof  31398  fneval  31517  relowlpssretop  32388  phpreu  32563  poimirlem26  32605  brnonrel  36914  brcofffn  37349  brco2f1o  37350  brco3f1o  37351  clsneikex  37424  clsneinex  37425  clsneiel1  37426  neicvgmex  37435  neicvgel1  37437  climreeq  38680  rgrprop  40760  rusgrprop  40762  gte-lte  42264  gt-lt  42265  gte-lteh  42266  gt-lth  42267