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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2677 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 4584 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 4584 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 302 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ⟨cop 4131   class class class wbr 4583 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-br 4584 This theorem is referenced by:  breqi  4589  breqd  4594  poeq1  4962  soeq1  4978  freq1  5008  fveq1  6102  foeqcnvco  6455  f1eqcocnv  6456  isoeq2  6468  isoeq3  6469  brfvopab  6598  ofreq  6798  supeq3  8238  oieq1  8300  dcomex  9152  axdc2lem  9153  brdom3  9231  brdom7disj  9234  brdom6disj  9235  dfrtrclrec2  13645  rtrclreclem3  13648  relexpindlem  13651  rtrclind  13653  shftfval  13658  isprs  16753  isdrs  16757  ispos  16770  istos  16858  efglem  17952  frgpuplem  18008  ordtval  20803  utop2nei  21864  utop3cls  21865  isucn2  21893  ucnima  21895  iducn  21897  ex-opab  26681  resspos  28990  cureq  32555  poimirlem31  32610  poimir  32612  brabsb2  33165  rfovfvd  37316  fsovrfovd  37323  wlkbProp  40817
 Copyright terms: Public domain W3C validator