MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq Unicode version

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2530 . 2
2 df-br 4453 . 2
3 df-br 4453 . 2
41, 2, 33bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  <.cop 4035   class class class wbr 4452
This theorem is referenced by:  breqi  4458  breqd  4463  poeq1  4808  soeq1  4824  freq1  4854  fveq1  5870  foeqcnvco  6203  f1eqcocnv  6204  isoeq2  6216  isoeq3  6217  ofreq  6543  supeq3  7929  oieq1  7958  dcomex  8848  axdc2lem  8849  brdom3  8927  brdom7disj  8930  brdom6disj  8931  shftfval  12903  isprs  15559  isdrs  15563  ispos  15576  istos  15665  efglem  16734  frgpuplem  16790  ordtval  19690  utop2nei  20753  utop3cls  20754  isucn2  20782  ucnima  20784  iducn  20786  ex-opab  25153  resspos  27647  relexpindlem  29062  dfrtrclrec2  29066  rtrclreclem.trans  29069  rtrclind  29072  brabsb2  30603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-br 4453
  Copyright terms: Public domain W3C validator