Theorem breq 5099

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-br 5098

This theorem is referenced by:  breqi  5103  breqd  5108  poeq1  5534  soeq1  5552  freq1  5590  fveq1  6832  foeqcnvco  7246  f1eqcocnv  7247  isoeq2  7264  isoeq3  7265  eqfunresadj  7306  brfvopab  7415  ofreq  7626  supeq3  9354  oieq1  9419  ttrcleq  9620  dcomex  10359  axdc2lem  10360  brdom3  10440  brdom7disj  10443  brdom6disj  10444  dfrtrclrec2  14983  relexpindlem  14988  rtrclind  14990  shftfval  14995  isprs  18221  isdrs  18226  ispos  18239  istos  18341  resspos  18354  chneq1  18537  efglem  19647  frgpuplem  19703  ordtval  23135  utop2nei  24196  utop3cls  24197  isucn2  24224  ucnima  24226  iducn  24228  ex-opab  30488  acycgr0v  35321  prclisacycgr  35324  satf  35526  cureq  37766  poimirlem31  37821  poimir  37823  cosseq  38686  elrefrels3  38769  elcnvrefrels3  38785  elsymrels3  38808  elsymrels5  38810  eltrrels3  38834  eleqvrels3  38847  brabsb2  39157  rfovfvd  44280  fsovrfovd  44287  relpeq2  45223  relpeq3  45224  sprsymrelf  47778  sprsymrelfo  47780  upwlkbprop  48421