Theorem breq 5104

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5103

This theorem is referenced by:  breqi  5108  breqd  5113  poeq1  5542  soeq1  5560  freq1  5598  fveq1  6839  foeqcnvco  7257  f1eqcocnv  7258  isoeq2  7275  isoeq3  7276  eqfunresadj  7317  brfvopab  7426  ofreq  7637  supeq3  9376  oieq1  9441  ttrcleq  9638  dcomex  10376  axdc2lem  10377  brdom3  10457  brdom7disj  10460  brdom6disj  10461  dfrtrclrec2  15000  relexpindlem  15005  rtrclind  15007  shftfval  15012  isprs  18237  isdrs  18242  ispos  18255  istos  18357  resspos  18370  efglem  19630  frgpuplem  19686  ordtval  23109  utop2nei  24171  utop3cls  24172  isucn2  24199  ucnima  24201  iducn  24203  ex-opab  30411  acycgr0v  35128  prclisacycgr  35131  satf  35333  cureq  37583  poimirlem31  37638  poimir  37640  cosseq  38410  elrefrels3  38503  elcnvrefrels3  38519  elsymrels3  38538  elsymrels5  38540  eltrrels3  38564  eleqvrels3  38577  brabsb2  38848  rfovfvd  43984  fsovrfovd  43991  relpeq2  44928  relpeq3  44929  sprsymrelf  47489  sprsymrelfo  47491  upwlkbprop  48119