Theorem breq 4007

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 2241	. 2 |- ( R = S -> ( <. A , B >. e. R <-> <. A , B >. e. S ) )
2		df-br 4006	. 2 |- ( A R B <-> <. A , B >. e. R )
3		df-br 4006	. 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 1353   e. wcel 2148   <.cop 3597   class class class wbr 4005

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-br 4006

This theorem is referenced by:  breqi  4011  breqd  4016  poeq1  4301  soeq1  4317  frforeq1  4345  weeq1  4358  fveq1  5516  foeqcnvco  5793  f1eqcocnv  5794  isoeq2  5805  isoeq3  5806  ofreq  6088  supeq3  6991  tapeq1  7253  shftfvalg  10829  shftfval  10832  pw1nct  14837