Theorem breq 5121

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ⟨cop 4607   class class class wbr 5119

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-br 5120

This theorem is referenced by:  breqi  5125  breqd  5130  poeq1  5564  soeq1  5582  freq1  5621  fveq1  6875  foeqcnvco  7293  f1eqcocnv  7294  isoeq2  7311  isoeq3  7312  eqfunresadj  7353  brfvopab  7464  ofreq  7675  supeq3  9461  oieq1  9526  ttrcleq  9723  dcomex  10461  axdc2lem  10462  brdom3  10542  brdom7disj  10545  brdom6disj  10546  dfrtrclrec2  15077  relexpindlem  15082  rtrclind  15084  shftfval  15089  isprs  18308  isdrs  18313  ispos  18326  istos  18428  efglem  19697  frgpuplem  19753  ordtval  23127  utop2nei  24189  utop3cls  24190  isucn2  24217  ucnima  24219  iducn  24221  ex-opab  30413  resspos  32946  acycgr0v  35170  prclisacycgr  35173  satf  35375  cureq  37620  poimirlem31  37675  poimir  37677  cosseq  38444  elrefrels3  38537  elcnvrefrels3  38553  elsymrels3  38572  elsymrels5  38574  eltrrels3  38598  eleqvrels3  38611  brabsb2  38880  rfovfvd  44026  fsovrfovd  44033  relpeq2  44970  relpeq3  44971  sprsymrelf  47509  sprsymrelfo  47511  upwlkbprop  48113