Theorem breq 5087

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-br 5086

This theorem is referenced by:  breqi  5091  breqd  5096  poeq1  5542  soeq1  5560  freq1  5598  fveq1  6839  foeqcnvco  7255  f1eqcocnv  7256  isoeq2  7273  isoeq3  7274  eqfunresadj  7315  brfvopab  7424  ofreq  7635  supeq3  9362  oieq1  9427  ttrcleq  9630  dcomex  10369  axdc2lem  10370  brdom3  10450  brdom7disj  10453  brdom6disj  10454  dfrtrclrec2  15020  relexpindlem  15025  rtrclind  15027  shftfval  15032  isprs  18262  isdrs  18267  ispos  18280  istos  18382  resspos  18395  chneq1  18578  efglem  19691  frgpuplem  19747  ordtval  23154  utop2nei  24215  utop3cls  24216  isucn2  24243  ucnima  24245  iducn  24247  ex-opab  30502  acycgr0v  35330  prclisacycgr  35333  satf  35535  cureq  37917  poimirlem31  37972  poimir  37974  cosseq  38837  elrefrels3  38920  elcnvrefrels3  38936  elsymrels3  38959  elsymrels5  38961  eltrrels3  38985  eleqvrels3  38998  brabsb2  39308  rfovfvd  44429  fsovrfovd  44436  relpeq2  45372  relpeq3  45373  sprsymrelf  47955  sprsymrelfo  47957  upwlkbprop  48614