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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2414 . 2
2 df-br 4640 . 2
3 df-br 4640 . 2
41, 2, 33bitr4g 279 1
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-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 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