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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2158 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 3868 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 3868 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 222 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1296  wcel 1445  cop 3469   class class class wbr 3867
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091  df-br 3868
This theorem is referenced by:  breqi  3873  breqd  3878  poeq1  4150  soeq1  4166  frforeq1  4194  weeq1  4207  fveq1  5339  foeqcnvco  5607  f1eqcocnv  5608  isoeq2  5619  isoeq3  5620  ofreq  5897  supeq3  6765  shftfvalg  10383  shftfval  10386
  Copyright terms: Public domain W3C validator