Theorem breq 5072

Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)

Assertion

Ref	Expression
breq	⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))

Proof of Theorem breq

Step	Hyp	Ref	Expression
1		eleq2 2827	. 2 ⊢ (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5071	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3		df-br 5071	. 2 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
4	1, 2, 3	3bitr4g 313	1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-br 5071

This theorem is referenced by:  breqi  5076  breqd  5081  poeq1  5497  soeq1  5515  freq1  5550  fveq1  6755  foeqcnvco  7152  f1eqcocnv  7153  f1eqcocnvOLD  7154  isoeq2  7169  isoeq3  7170  brfvopab  7310  ofreq  7515  supeq3  9138  oieq1  9201  dcomex  10134  axdc2lem  10135  brdom3  10215  brdom7disj  10218  brdom6disj  10219  dfrtrclrec2  14697  relexpindlem  14702  rtrclind  14704  shftfval  14709  isprs  17930  isdrs  17934  ispos  17947  istos  18051  efglem  19237  frgpuplem  19293  ordtval  22248  utop2nei  23310  utop3cls  23311  isucn2  23339  ucnima  23341  iducn  23343  ex-opab  28697  resspos  31146  acycgr0v  33010  prclisacycgr  33013  satf  33215  eqfunresadj  33641  ttrcleq  33695  cureq  35680  poimirlem31  35735  poimir  35737  cosseq  36476  elrefrels3  36563  elcnvrefrels3  36576  elsymrels3  36595  elsymrels5  36597  eltrrels3  36621  eleqvrels3  36633  brabsb2  36803  rfovfvd  41499  fsovrfovd  41506  sprsymrelf  44835  sprsymrelfo  44837  upwlkbprop  45188