Theorem breq 4003

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 4002	. 2 |- ( A R B <-> <. A , B >. e. R )
3		df-br 4002	. 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 3595   class class class wbr 4001

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 4002

This theorem is referenced by:  breqi  4007  breqd  4012  poeq1  4297  soeq1  4313  frforeq1  4341  weeq1  4354  fveq1  5511  foeqcnvco  5786  f1eqcocnv  5787  isoeq2  5798  isoeq3  5799  ofreq  6081  supeq3  6984  tapeq1  7246  shftfvalg  10818  shftfval  10821  pw1nct  14523