Theorem breqi 4398

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 4394	. 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 1370   class class class wbr 4392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446  df-br 4393

This theorem is referenced by:  f1ompt  5966  isocnv3  6124  brtpos2  6853  brwitnlem  7049  brdifun  7230  omxpenlem  7514  infxpenlem  8283  ltpiord  9159  nqerf  9202  nqerid  9205  ordpinq  9215  ltxrlt  9548  ltxr  11198  oduleg  15406  oduposb  15410  meet0  15411  join0  15412  xmeterval  20125  pi1cpbl  20734  brbtwn  23282  avril1  23793  axhcompl-zf  24537  hlimadd  24732  hhcmpl  24739  hhcms  24742  hlim0  24775  posrasymb  26254  trleile  26263  isarchi  26335  pstmfval  26459  pstmxmet  26460  lmlim  26513  brtxp  28047  brpprod  28052  brpprod3b  28054  brtxpsd2  28062  brdomain  28100  brrange  28101  brimg  28104  brapply  28105  brsuccf  28108  brrestrict  28116  brub  28121  brlb  28122  colineardim1  28228  broutsideof  28288  fneval  28699  climreeq  29926  rgraprop  30685  rusgraprop  30686  rusgrargra  30687  gte-lte  31357  gt-lt  31358  gte-lteh  31359  gt-lth  31360