Theorem breq 4454

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

Assertion

Ref	Expression
breq

Proof of Theorem breq

Step	Hyp	Ref	Expression
1		eleq2 2530	. 2
2		df-br 4453	. 2
3		df-br 4453	. 2
4	1, 2, 3	3bitr4g 288	1

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