Theorem breq 5102

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

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

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 5101

This theorem is referenced by:  breqi  5106  breqd  5111  poeq1  5545  soeq1  5563  freq1  5601  fveq1  6843  foeqcnvco  7258  f1eqcocnv  7259  isoeq2  7276  isoeq3  7277  eqfunresadj  7318  brfvopab  7427  ofreq  7638  supeq3  9366  oieq1  9431  ttrcleq  9632  dcomex  10371  axdc2lem  10372  brdom3  10452  brdom7disj  10455  brdom6disj  10456  dfrtrclrec2  14995  relexpindlem  15000  rtrclind  15002  shftfval  15007  isprs  18233  isdrs  18238  ispos  18251  istos  18353  resspos  18366  chneq1  18549  efglem  19662  frgpuplem  19718  ordtval  23150  utop2nei  24211  utop3cls  24212  isucn2  24239  ucnima  24241  iducn  24243  ex-opab  30525  acycgr0v  35370  prclisacycgr  35373  satf  35575  cureq  37876  poimirlem31  37931  poimir  37933  cosseq  38796  elrefrels3  38879  elcnvrefrels3  38895  elsymrels3  38918  elsymrels5  38920  eltrrels3  38944  eleqvrels3  38957  brabsb2  39267  rfovfvd  44387  fsovrfovd  44394  relpeq2  45330  relpeq3  45331  sprsymrelf  47884  sprsymrelfo  47886  upwlkbprop  48527