New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  breq GIF version

Theorem breq 4641
 Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
Assertion
Ref Expression
breq (R = S → (ARBASB))

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2414 . 2 (R = S → (A, B RA, B S))
2 df-br 4640 . 2 (ARBA, B R)
3 df-br 4640 . 2 (ASBA, B S)
41, 2, 33bitr4g 279 1 (R = S → (ARBASB))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710  ⟨cop 4561   class class class wbr 4639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4640 This theorem is referenced by:  breqi  4645  breqd  4650  imaeq1  4937  fveq1  5327  isoeq2  5483  isoeq3  5484  clos1basesucg  5884  trd  5921  frd  5922  extd  5923  symd  5924  trrd  5925  refrd  5926  refd  5927  antird  5928  antid  5929  connexrd  5930  connexd  5931  iserd  5942
 Copyright terms: Public domain W3C validator