Theorem breq 5101

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ⟨cop 4587   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-br 5100

This theorem is referenced by:  breqi  5105  breqd  5110  poeq1  5536  soeq1  5554  freq1  5592  fveq1  6834  foeqcnvco  7248  f1eqcocnv  7249  isoeq2  7266  isoeq3  7267  eqfunresadj  7308  brfvopab  7417  ofreq  7628  supeq3  9356  oieq1  9421  ttrcleq  9622  dcomex  10361  axdc2lem  10362  brdom3  10442  brdom7disj  10445  brdom6disj  10446  dfrtrclrec2  14985  relexpindlem  14990  rtrclind  14992  shftfval  14997  isprs  18223  isdrs  18228  ispos  18241  istos  18343  resspos  18356  chneq1  18539  efglem  19649  frgpuplem  19705  ordtval  23137  utop2nei  24198  utop3cls  24199  isucn2  24226  ucnima  24228  iducn  24230  ex-opab  30511  acycgr0v  35344  prclisacycgr  35347  satf  35549  cureq  37799  poimirlem31  37854  poimir  37856  cosseq  38719  elrefrels3  38802  elcnvrefrels3  38818  elsymrels3  38841  elsymrels5  38843  eltrrels3  38867  eleqvrels3  38880  brabsb2  39190  rfovfvd  44310  fsovrfovd  44317  relpeq2  45253  relpeq3  45254  sprsymrelf  47808  sprsymrelfo  47810  upwlkbprop  48451