Theorem breq 5104

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

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

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 5103

This theorem is referenced by:  breqi  5108  breqd  5113  poeq1  5542  soeq1  5560  freq1  5598  fveq1  6839  foeqcnvco  7257  f1eqcocnv  7258  isoeq2  7275  isoeq3  7276  eqfunresadj  7317  brfvopab  7426  ofreq  7637  supeq3  9376  oieq1  9441  ttrcleq  9640  dcomex  10378  axdc2lem  10379  brdom3  10459  brdom7disj  10462  brdom6disj  10463  dfrtrclrec2  15001  relexpindlem  15006  rtrclind  15008  shftfval  15013  isprs  18238  isdrs  18243  ispos  18256  istos  18358  resspos  18371  efglem  19631  frgpuplem  19687  ordtval  23110  utop2nei  24172  utop3cls  24173  isucn2  24200  ucnima  24202  iducn  24204  ex-opab  30412  acycgr0v  35129  prclisacycgr  35132  satf  35334  cureq  37584  poimirlem31  37639  poimir  37641  cosseq  38411  elrefrels3  38504  elcnvrefrels3  38520  elsymrels3  38539  elsymrels5  38541  eltrrels3  38565  eleqvrels3  38578  brabsb2  38849  rfovfvd  43985  fsovrfovd  43992  relpeq2  44929  relpeq3  44930  sprsymrelf  47490  sprsymrelfo  47492  upwlkbprop  48120