Theorem breq 5147

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  ⟨cop 4631   class class class wbr 5145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  df-br 5146

This theorem is referenced by:  breqi  5151  breqd  5156  poeq1  5589  soeq1  5607  freq1  5644  fveq1  6891  foeqcnvco  7305  f1eqcocnv  7306  isoeq2  7321  isoeq3  7322  eqfunresadj  7363  brfvopab  7473  ofreq  7685  supeq3  9484  oieq1  9547  ttrcleq  9744  dcomex  10480  axdc2lem  10481  brdom3  10561  brdom7disj  10564  brdom6disj  10565  dfrtrclrec2  15057  relexpindlem  15062  rtrclind  15064  shftfval  15069  isprs  18316  isdrs  18320  ispos  18333  istos  18437  efglem  19709  frgpuplem  19765  ordtval  23180  utop2nei  24242  utop3cls  24243  isucn2  24271  ucnima  24273  iducn  24275  ex-opab  30361  resspos  32838  acycgr0v  34988  prclisacycgr  34991  satf  35193  cureq  37309  poimirlem31  37364  poimir  37366  cosseq  38136  elrefrels3  38229  elcnvrefrels3  38245  elsymrels3  38264  elsymrels5  38266  eltrrels3  38290  eleqvrels3  38303  brabsb2  38572  rfovfvd  43705  fsovrfovd  43712  sprsymrelf  47102  sprsymrelfo  47104  upwlkbprop  47550