Theorem breq 5109

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

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

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 5108

This theorem is referenced by:  breqi  5113  breqd  5118  poeq1  5549  soeq1  5567  freq1  5605  fveq1  6857  foeqcnvco  7275  f1eqcocnv  7276  isoeq2  7293  isoeq3  7294  eqfunresadj  7335  brfvopab  7446  ofreq  7657  supeq3  9400  oieq1  9465  ttrcleq  9662  dcomex  10400  axdc2lem  10401  brdom3  10481  brdom7disj  10484  brdom6disj  10485  dfrtrclrec2  15024  relexpindlem  15029  rtrclind  15031  shftfval  15036  isprs  18257  isdrs  18262  ispos  18275  istos  18377  efglem  19646  frgpuplem  19702  ordtval  23076  utop2nei  24138  utop3cls  24139  isucn2  24166  ucnima  24168  iducn  24170  ex-opab  30361  resspos  32892  acycgr0v  35135  prclisacycgr  35138  satf  35340  cureq  37590  poimirlem31  37645  poimir  37647  cosseq  38417  elrefrels3  38510  elcnvrefrels3  38526  elsymrels3  38545  elsymrels5  38547  eltrrels3  38571  eleqvrels3  38584  brabsb2  38855  rfovfvd  43991  fsovrfovd  43998  relpeq2  44935  relpeq3  44936  sprsymrelf  47496  sprsymrelfo  47498  upwlkbprop  48126