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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2687 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4624 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4624 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 303 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1987  ⟨cop 4161   class class class wbr 4623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617  df-br 4624 This theorem is referenced by:  breqi  4629  breqd  4634  poeq1  5008  soeq1  5024  freq1  5054  fveq1  6157  foeqcnvco  6520  f1eqcocnv  6521  isoeq2  6533  isoeq3  6534  brfvopab  6665  ofreq  6865  supeq3  8315  oieq1  8377  dcomex  9229  axdc2lem  9230  brdom3  9310  brdom7disj  9313  brdom6disj  9314  dfrtrclrec2  13747  rtrclreclem3  13750  relexpindlem  13753  rtrclind  13755  shftfval  13760  isprs  16870  isdrs  16874  ispos  16887  istos  16975  efglem  18069  frgpuplem  18125  ordtval  20933  utop2nei  21994  utop3cls  21995  isucn2  22023  ucnima  22025  iducn  22027  ex-opab  27177  resspos  29486  sltgtres  31623  noextendltgt  31627  cureq  33056  poimirlem31  33111  poimir  33113  brabsb2  33666  rfovfvd  37817  fsovrfovd  37824  upwlkbprop  41037  sprsymrelf  41063  sprsymrelfo  41065
 Copyright terms: Public domain W3C validator