Theorem breqi 4424

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 4420	. 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 189   = wceq 1455   class class class wbr 4418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-cleq 2455  df-clel 2458  df-br 4419

This theorem is referenced by:  f1ompt  6072  isocnv3  6253  brtpos2  7010  brwitnlem  7240  brdifun  7421  omxpenlem  7704  infxpenlem  8475  ltpiord  9343  nqerf  9386  nqerid  9389  ordpinq  9399  ltxrlt  9735  ltxr  11449  trclublem  13114  oduleg  16433  oduposb  16437  meet0  16438  join0  16439  xmeterval  21502  pi1cpbl  22130  ltgov  24698  brbtwn  24985  rgraprop  25712  rusgraprop  25713  rusgrargra  25714  avril1  25956  axhcompl-zf  26707  hlimadd  26902  hhcmpl  26909  hhcms  26912  hlim0  26944  fcoinvbr  28268  posrasymb  28470  trleile  28479  isarchi  28550  pstmfval  28750  pstmxmet  28751  lmlim  28804  brtxp  30697  brpprod  30702  brpprod3b  30704  brtxpsd2  30712  brdomain  30750  brrange  30751  brimg  30754  brapply  30755  brsuccf  30758  brrestrict  30766  brub  30771  brlb  30772  colineardim1  30878  broutsideof  30938  fneval  31058  relowlpssretop  31813  phpreu  31975  poimirlem26  32012  brnonrel  36241  climreeq  37779  rgrprop  39724  rusgrprop  39726  gte-lte  40813  gt-lt  40814  gte-lteh  40815  gt-lth  40816