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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2827 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5105 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 5105 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 314 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  cop 4591   class class class wbr 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-clel 2816  df-br 5105
This theorem is referenced by:  breqi  5110  breqd  5115  poeq1  5546  soeq1  5564  freq1  5601  fveq1  6837  foeqcnvco  7241  f1eqcocnv  7242  f1eqcocnvOLD  7243  isoeq2  7258  isoeq3  7259  eqfunresadj  7300  brfvopab  7407  ofreq  7612  supeq3  9319  oieq1  9382  ttrcleq  9579  dcomex  10317  axdc2lem  10318  brdom3  10398  brdom7disj  10401  brdom6disj  10402  dfrtrclrec2  14878  relexpindlem  14883  rtrclind  14885  shftfval  14890  isprs  18122  isdrs  18126  ispos  18139  istos  18243  efglem  19433  frgpuplem  19489  ordtval  22468  utop2nei  23530  utop3cls  23531  isucn2  23559  ucnima  23561  iducn  23563  ex-opab  29181  resspos  31627  acycgr0v  33522  prclisacycgr  33525  satf  33727  cureq  35985  poimirlem31  36040  poimir  36042  cosseq  36819  elrefrels3  36912  elcnvrefrels3  36928  elsymrels3  36947  elsymrels5  36949  eltrrels3  36973  eleqvrels3  36986  brabsb2  37255  rfovfvd  42073  fsovrfovd  42080  sprsymrelf  45478  sprsymrelfo  45480  upwlkbprop  45831
  Copyright terms: Public domain W3C validator