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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2253 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4019 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4019 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 223 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1364  wcel 2160  cop 3610   class class class wbr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-br 4019
This theorem is referenced by:  breqi  4024  breqd  4029  poeq1  4314  soeq1  4330  frforeq1  4358  weeq1  4371  fveq1  5529  foeqcnvco  5807  f1eqcocnv  5808  isoeq2  5819  isoeq3  5820  ofreq  6104  supeq3  7007  tapeq1  7269  shftfvalg  10845  shftfval  10848  pw1nct  15150
  Copyright terms: Public domain W3C validator