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

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

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2881 . 2 (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5034 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3 df-br 5034 . 2 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
41, 2, 33bitr4g 317 1 (𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2112  ⟨cop 4534   class class class wbr 5033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873  df-br 5034 This theorem is referenced by:  breqi  5039  breqd  5044  poeq1  5445  soeq1  5462  freq1  5493  fveq1  6648  foeqcnvco  7038  f1eqcocnv  7039  f1eqcocnvOLD  7040  isoeq2  7054  isoeq3  7055  brfvopab  7194  ofreq  7396  supeq3  8901  oieq1  8964  dcomex  9862  axdc2lem  9863  brdom3  9943  brdom7disj  9946  brdom6disj  9947  dfrtrclrec2  14411  relexpindlem  14417  rtrclind  14419  shftfval  14424  isprs  17535  isdrs  17539  ispos  17552  istos  17640  efglem  18837  frgpuplem  18893  ordtval  21797  utop2nei  22859  utop3cls  22860  isucn2  22888  ucnima  22890  iducn  22892  ex-opab  28220  resspos  30675  acycgr0v  32503  prclisacycgr  32506  satf  32708  eqfunresadj  33112  cureq  35026  poimirlem31  35081  poimir  35083  cosseq  35824  elrefrels3  35911  elcnvrefrels3  35924  elsymrels3  35943  elsymrels5  35945  eltrrels3  35969  eleqvrels3  35981  brabsb2  36151  rfovfvd  40690  fsovrfovd  40697  sprsymrelf  43999  sprsymrelfo  44001  upwlkbprop  44353
 Copyright terms: Public domain W3C validator