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

Theorem breq 5059
Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
Assertion
Ref Expression
breq (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2898 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5058 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 5058 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 315 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  cop 4563   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-br 5058
This theorem is referenced by:  breqi  5063  breqd  5068  poeq1  5470  soeq1  5487  freq1  5518  fveq1  6662  foeqcnvco  7047  f1eqcocnv  7048  isoeq2  7060  isoeq3  7061  brfvopab  7200  ofreq  7401  supeq3  8901  oieq1  8964  dcomex  9857  axdc2lem  9858  brdom3  9938  brdom7disj  9941  brdom6disj  9942  dfrtrclrec2  14404  relexpindlem  14410  rtrclind  14412  shftfval  14417  isprs  17528  isdrs  17532  ispos  17545  istos  17633  efglem  18771  frgpuplem  18827  ordtval  21725  utop2nei  22786  utop3cls  22787  isucn2  22815  ucnima  22817  iducn  22819  ex-opab  28138  resspos  30573  acycgr0v  32292  prclisacycgr  32295  satf  32497  eqfunresadj  32901  cureq  34749  poimirlem31  34804  poimir  34806  cosseq  35551  elrefrels3  35638  elcnvrefrels3  35651  elsymrels3  35670  elsymrels5  35672  eltrrels3  35696  eleqvrels3  35708  brabsb2  35878  rfovfvd  40226  fsovrfovd  40233  sprsymrelf  43534  sprsymrelfo  43536  upwlkbprop  43890
  Copyright terms: Public domain W3C validator