Theorem breq 4642

Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)

Assertion

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

Proof of Theorem breq

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

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710  <.cop 4562   class class class wbr 4640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349  df-br 4641

This theorem is referenced by:  breqi  4646  breqd  4651  imaeq1  4938  fveq1  5328  isoeq2  5484  isoeq3  5485  clos1basesucg  5885  trd  5922  frd  5923  extd  5924  symd  5925  trrd  5926  refrd  5927  refd  5928  antird  5929  antid  5930  connexrd  5931  connexd  5932  iserd  5943