Theorem breq 4104

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2203   <.cop 3685   class class class wbr 4102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-br 4103

This theorem is referenced by:  breqi  4108  breqd  4113  poeq1  4411  soeq1  4427  frforeq1  4455  weeq1  4468  fveq1  5660  foeqcnvco  5954  f1eqcocnv  5955  isoeq2  5966  isoeq3  5967  ofreq  6261  supeq3  7272  tapeq1  7554  shftfvalg  11481  shftfval  11484  pw1nct  16747