Theorem breq 5112

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-br 5111

This theorem is referenced by:  breqi  5116  breqd  5121  poeq1  5552  soeq1  5570  freq1  5608  fveq1  6860  foeqcnvco  7278  f1eqcocnv  7279  isoeq2  7296  isoeq3  7297  eqfunresadj  7338  brfvopab  7449  ofreq  7660  supeq3  9407  oieq1  9472  ttrcleq  9669  dcomex  10407  axdc2lem  10408  brdom3  10488  brdom7disj  10491  brdom6disj  10492  dfrtrclrec2  15031  relexpindlem  15036  rtrclind  15038  shftfval  15043  isprs  18264  isdrs  18269  ispos  18282  istos  18384  efglem  19653  frgpuplem  19709  ordtval  23083  utop2nei  24145  utop3cls  24146  isucn2  24173  ucnima  24175  iducn  24177  ex-opab  30368  resspos  32899  acycgr0v  35142  prclisacycgr  35145  satf  35347  cureq  37597  poimirlem31  37652  poimir  37654  cosseq  38424  elrefrels3  38517  elcnvrefrels3  38533  elsymrels3  38552  elsymrels5  38554  eltrrels3  38578  eleqvrels3  38591  brabsb2  38862  rfovfvd  43998  fsovrfovd  44005  relpeq2  44942  relpeq3  44943  sprsymrelf  47500  sprsymrelfo  47502  upwlkbprop  48130