Theorem breqi 4448

Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)

Hypothesis

Ref	Expression
breqi.1	|- R = S

Assertion

Ref	Expression
breqi	|- ( A R B <-> A S B )

Proof of Theorem breqi

Step	Hyp	Ref	Expression
1		breqi.1	. 2 |- R = S
2		breq 4444	. 2 |- ( R = S -> ( A R B <-> A S B ) )
3	1, 2	ax-mp 5	1 |- ( A R B <-> A S B )

Syntax hints:   <-> wb 184   = wceq 1374   class class class wbr 4442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2454  df-clel 2457  df-br 4443

This theorem is referenced by:  f1ompt  6036  isocnv3  6209  brtpos2  6953  brwitnlem  7149  brdifun  7330  omxpenlem  7610  infxpenlem  8382  ltpiord  9256  nqerf  9299  nqerid  9302  ordpinq  9312  ltxrlt  9646  ltxr  11315  oduleg  15610  oduposb  15614  meet0  15615  join0  15616  xmeterval  20665  pi1cpbl  21274  ltgov  23705  brbtwn  23873  rgraprop  24592  rusgraprop  24593  rusgrargra  24594  avril1  24835  axhcompl-zf  25579  hlimadd  25774  hhcmpl  25781  hhcms  25784  hlim0  25817  fcoinvbr  27122  posrasymb  27295  trleile  27304  isarchi  27376  pstmfval  27499  pstmxmet  27500  lmlim  27553  brtxp  29095  brpprod  29100  brpprod3b  29102  brtxpsd2  29110  brdomain  29148  brrange  29149  brimg  29152  brapply  29153  brsuccf  29156  brrestrict  29164  brub  29169  brlb  29170  colineardim1  29276  broutsideof  29336  fneval  29748  climreeq  31112  gte-lte  32076  gt-lt  32077  gte-lteh  32078  gt-lth  32079  trclubg  36672