Theorem breq 4655

Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)

Assertion

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

Proof of Theorem breq

Step	Hyp	Ref	Expression
1		eleq2 2690	. 2 |- ( R = S -> ( <. A , B >. e. R <-> <. A , B >. e. S ) )
2		df-br 4654	. 2 |- ( A R B <-> <. A , B >. e. R )
3		df-br 4654	. 2 |- ( A S B <-> <. A , B >. e. S )
4	1, 2, 3	3bitr4g 303	1 |- ( R = S -> ( A R B <-> A S B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   <.cop 4183   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-br 4654

This theorem is referenced by:  breqi  4659  breqd  4664  poeq1  5038  soeq1  5054  freq1  5084  fveq1  6190  foeqcnvco  6555  f1eqcocnv  6556  isoeq2  6568  isoeq3  6569  brfvopab  6700  ofreq  6900  supeq3  8355  oieq1  8417  dcomex  9269  axdc2lem  9270  brdom3  9350  brdom7disj  9353  brdom6disj  9354  dfrtrclrec2  13797  rtrclreclem3  13800  relexpindlem  13803  rtrclind  13805  shftfval  13810  isprs  16930  isdrs  16934  ispos  16947  istos  17035  efglem  18129  frgpuplem  18185  ordtval  20993  utop2nei  22054  utop3cls  22055  isucn2  22083  ucnima  22085  iducn  22087  ex-opab  27289  resspos  29659  eqfunresadj  31659  cureq  33385  poimirlem31  33440  poimir  33442  brabsb2  34147  rfovfvd  38296  fsovrfovd  38303  upwlkbprop  41719  sprsymrelf  41745  sprsymrelfo  41747