Theorem breq 4964

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 2871	. 2 ⊢ (𝑅 = 𝑆 → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 4963	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
3		df-br 4963	. 2 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
4	1, 2, 3	3bitr4g 315	1 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522   ∈ wcel 2081  ⟨cop 4478   class class class wbr 4962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863  df-br 4963

This theorem is referenced by:  breqi  4968  breqd  4973  poeq1  5365  soeq1  5382  freq1  5413  fveq1  6537  foeqcnvco  6921  f1eqcocnv  6922  isoeq2  6934  isoeq3  6935  brfvopab  7070  ofreq  7270  supeq3  8759  oieq1  8822  dcomex  9715  axdc2lem  9716  brdom3  9796  brdom7disj  9799  brdom6disj  9800  dfrtrclrec2  14250  relexpindlem  14256  rtrclind  14258  shftfval  14263  isprs  17369  isdrs  17373  ispos  17386  istos  17474  efglem  18569  frgpuplem  18625  ordtval  21481  utop2nei  22542  utop3cls  22543  isucn2  22571  ucnima  22573  iducn  22575  ex-opab  27903  resspos  30320  acycgr0v  32004  prclisacycgr  32007  satf  32209  eqfunresadj  32613  cureq  34418  poimirlem31  34473  poimir  34475  cosseq  35221  elrefrels3  35308  elcnvrefrels3  35321  elsymrels3  35340  elsymrels5  35342  eltrrels3  35366  eleqvrels3  35378  brabsb2  35548  rfovfvd  39852  fsovrfovd  39859  sprsymrelf  43159  sprsymrelfo  43161  upwlkbprop  43515