Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq GIF version

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2179 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 3898 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 3898 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 222 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1314   ∈ wcel 1463  ⟨cop 3498   class class class wbr 3897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-br 3898 This theorem is referenced by:  breqi  3903  breqd  3908  poeq1  4189  soeq1  4205  frforeq1  4233  weeq1  4246  fveq1  5386  foeqcnvco  5657  f1eqcocnv  5658  isoeq2  5669  isoeq3  5670  ofreq  5951  supeq3  6843  shftfvalg  10530  shftfval  10533
 Copyright terms: Public domain W3C validator