Theorem breq 2621

Description: Equality theorem for binary relations.

Assertion

Ref	Expression
breq	|- (R = S -> (ARB <-> ASB))

Proof of Theorem breq

Step	Hyp	Ref	Expression
1		eleq2 1535	. 2 |- (R = S -> (<.A, B>. e. R <-> <.A, B>. e. S))
2		df-br 2620	. 2 |- (ARB <-> <.A, B>. e. R)
3		df-br 2620	. 2 |- (ASB <-> <.A, B>. e. S)
4	1, 2, 3	3bitr4g 555	1 |- (R = S -> (ARB <-> ASB))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  <.cop 2411   class class class wbr 2619

This theorem is referenced by:  breqi 2625  hbbrd 2659  sbcbrg 2662  sbcbr12g 2663  poeq1 2842  soeq1 2853  freq1 2922  coeq1 3281  coeq2 3282  isoeq2 3888  isoeq3 3889  brdom3 4801  brdom7disj 4804  brdom6disj 4805  lmbr 7928  iscms 7946  spwval2 8653

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472  df-br 2620

Copyright terms: Public domain