Theorem breq 5094

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ⟨cop 4583   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5093

This theorem is referenced by:  breqi  5098  breqd  5103  poeq1  5530  soeq1  5548  freq1  5586  fveq1  6821  foeqcnvco  7237  f1eqcocnv  7238  isoeq2  7255  isoeq3  7256  eqfunresadj  7297  brfvopab  7406  ofreq  7617  supeq3  9339  oieq1  9404  ttrcleq  9605  dcomex  10341  axdc2lem  10342  brdom3  10422  brdom7disj  10425  brdom6disj  10426  dfrtrclrec2  14965  relexpindlem  14970  rtrclind  14972  shftfval  14977  isprs  18202  isdrs  18207  ispos  18220  istos  18322  resspos  18335  efglem  19595  frgpuplem  19651  ordtval  23074  utop2nei  24136  utop3cls  24137  isucn2  24164  ucnima  24166  iducn  24168  ex-opab  30380  acycgr0v  35141  prclisacycgr  35144  satf  35346  cureq  37596  poimirlem31  37651  poimir  37653  cosseq  38423  elrefrels3  38516  elcnvrefrels3  38532  elsymrels3  38551  elsymrels5  38553  eltrrels3  38577  eleqvrels3  38590  brabsb2  38861  rfovfvd  43995  fsovrfovd  44002  relpeq2  44939  relpeq3  44940  sprsymrelf  47499  sprsymrelfo  47501  upwlkbprop  48142