Theorem breqi 4423

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 4419	. 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 187   = wceq 1437   class class class wbr 4417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2412  df-clel 2415  df-br 4418

This theorem is referenced by:  f1ompt  6051  isocnv3  6230  brtpos2  6979  brwitnlem  7209  brdifun  7390  omxpenlem  7671  infxpenlem  8441  ltpiord  9308  nqerf  9351  nqerid  9354  ordpinq  9364  ltxrlt  9700  ltxr  11411  trclublem  13038  oduleg  16356  oduposb  16360  meet0  16361  join0  16362  xmeterval  21424  pi1cpbl  22052  ltgov  24619  brbtwn  24906  rgraprop  25632  rusgraprop  25633  rusgrargra  25634  avril1  25876  axhcompl-zf  26627  hlimadd  26822  hhcmpl  26829  hhcms  26832  hlim0  26864  fcoinvbr  28195  posrasymb  28405  trleile  28414  isarchi  28487  pstmfval  28688  pstmxmet  28689  lmlim  28742  brtxp  30633  brpprod  30638  brpprod3b  30640  brtxpsd2  30648  brdomain  30686  brrange  30687  brimg  30690  brapply  30691  brsuccf  30694  brrestrict  30702  brub  30707  brlb  30708  colineardim1  30814  broutsideof  30874  fneval  30994  relowlpssretop  31702  phpreu  31837  poimirlem26  31874  climreeq  37480  gte-lte  39509  gt-lt  39510  gte-lteh  39511  gt-lth  39512