Theorem breq 4113

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 2298	. 2 |- ( R = S -> ( <. A , B >. e. R <-> <. A , B >. e. S ) )
2		df-br 4112	. 2 |- ( A R B <-> <. A , B >. e. R )
3		df-br 4112	. 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 2205   <.cop 3694   class class class wbr 4111

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-br 4112

This theorem is referenced by:  breqi  4117  breqd  4122  poeq1  4422  soeq1  4438  frforeq1  4466  weeq1  4479  fveq1  5671  foeqcnvco  5965  f1eqcocnv  5966  isoeq2  5977  isoeq3  5978  ofreq  6272  supeq3  7283  tapeq1  7568  shftfvalg  11507  shftfval  11510  pw1nct  16794