Theorem breq 5095

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ⟨cop 4581   class class class wbr 5093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-br 5094

This theorem is referenced by:  breqi  5099  breqd  5104  poeq1  5530  soeq1  5548  freq1  5586  fveq1  6827  foeqcnvco  7240  f1eqcocnv  7241  isoeq2  7258  isoeq3  7259  eqfunresadj  7300  brfvopab  7409  ofreq  7620  supeq3  9339  oieq1  9404  ttrcleq  9605  dcomex  10344  axdc2lem  10345  brdom3  10425  brdom7disj  10428  brdom6disj  10429  dfrtrclrec2  14971  relexpindlem  14976  rtrclind  14978  shftfval  14983  isprs  18208  isdrs  18213  ispos  18226  istos  18328  resspos  18341  chneq1  18524  efglem  19634  frgpuplem  19690  ordtval  23110  utop2nei  24171  utop3cls  24172  isucn2  24199  ucnima  24201  iducn  24203  ex-opab  30419  acycgr0v  35199  prclisacycgr  35202  satf  35404  cureq  37642  poimirlem31  37697  poimir  37699  cosseq  38534  elrefrels3  38617  elcnvrefrels3  38633  elsymrels3  38656  elsymrels5  38658  eltrrels3  38682  eleqvrels3  38695  brabsb2  38967  rfovfvd  44100  fsovrfovd  44107  relpeq2  45043  relpeq3  45044  sprsymrelf  47600  sprsymrelfo  47602  upwlkbprop  48243