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  14877  relexpindlem  14882  rtrclind  14884  shftfval  14889  isprs  18121  isdrs  18125  ispos  18138  istos  18242  efglem  19428  frgpuplem  19484  ordtval  22463  utop2nei  23525  utop3cls  23526  isucn2  23554  ucnima  23556  iducn  23558  ex-opab  29175  resspos  31621  acycgr0v  33516  prclisacycgr  33519  satf  33721  cureq  35950  poimirlem31  36005  poimir  36007  cosseq  36784  elrefrels3  36877  elcnvrefrels3  36893  elsymrels3  36912  elsymrels5  36914  eltrrels3  36938  eleqvrels3  36951  brabsb2  37220  rfovfvd  42037  fsovrfovd  42044  sprsymrelf  45442  sprsymrelfo  45444  upwlkbprop  45795
  Copyright terms: Public domain W3C validator