Theorem breqi 4400

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 4396	. 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 1405   class class class wbr 4394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397  df-br 4395

This theorem is referenced by:  f1ompt  5987  isocnv3  6167  brtpos2  6918  brwitnlem  7114  brdifun  7295  omxpenlem  7576  infxpenlem  8343  ltpiord  9215  nqerf  9258  nqerid  9261  ordpinq  9271  ltxrlt  9606  ltxr  11295  trclublem  12885  oduleg  15978  oduposb  15982  meet0  15983  join0  15984  xmeterval  21119  pi1cpbl  21728  ltgov  24259  brbtwn  24500  rgraprop  25226  rusgraprop  25227  rusgrargra  25228  avril1  25469  axhcompl-zf  26209  hlimadd  26404  hhcmpl  26411  hhcms  26414  hlim0  26447  fcoinvbr  27777  posrasymb  27977  trleile  27986  isarchi  28058  pstmfval  28208  pstmxmet  28209  lmlim  28262  brtxp  30191  brpprod  30196  brpprod3b  30198  brtxpsd2  30206  brdomain  30244  brrange  30245  brimg  30248  brapply  30249  brsuccf  30252  brrestrict  30260  brub  30265  brlb  30266  colineardim1  30372  broutsideof  30432  fneval  30568  climreeq  36969  gte-lte  38744  gt-lt  38745  gte-lteh  38746  gt-lth  38747