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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2673 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4575 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4575 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 301 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  cop 4127   class class class wbr 4574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2599  df-clel 2602  df-br 4575
This theorem is referenced by:  breqi  4580  breqd  4585  poeq1  4949  soeq1  4965  freq1  4995  fveq1  6084  foeqcnvco  6430  f1eqcocnv  6431  isoeq2  6443  isoeq3  6444  brfvopab  6573  ofreq  6772  supeq3  8212  oieq1  8274  dcomex  9126  axdc2lem  9127  brdom3  9205  brdom7disj  9208  brdom6disj  9209  dfrtrclrec2  13588  rtrclreclem3  13591  relexpindlem  13594  rtrclind  13596  shftfval  13601  isprs  16696  isdrs  16700  ispos  16713  istos  16801  efglem  17895  frgpuplem  17951  ordtval  20742  utop2nei  21803  utop3cls  21804  isucn2  21832  ucnima  21834  iducn  21836  ex-opab  26444  resspos  28793  cureq  32355  poimirlem31  32410  poimir  32412  brabsb2  32965  rfovfvd  37116  fsovrfovd  37123  wlkbProp  40816
  Copyright terms: Public domain W3C validator