Theorem breq 3967

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 2221	. 2 |- ( R = S -> ( <. A , B >. e. R <-> <. A , B >. e. S ) )
2		df-br 3966	. 2 |- ( A R B <-> <. A , B >. e. R )
3		df-br 3966	. 2 |- ( A S B <-> <. A , B >. e. S )
4	1, 2, 3	3bitr4g 222	1 |- ( R = S -> ( A R B <-> A S B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335   e. wcel 2128   <.cop 3563   class class class wbr 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-br 3966

This theorem is referenced by:  breqi  3971  breqd  3976  poeq1  4259  soeq1  4275  frforeq1  4303  weeq1  4316  fveq1  5467  foeqcnvco  5740  f1eqcocnv  5741  isoeq2  5752  isoeq3  5753  ofreq  6035  supeq3  6934  shftfvalg  10718  shftfval  10721  pw1nct  13586