Theorem breq 5076

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  ⟨cop 4568   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-br 5075

This theorem is referenced by:  breqi  5080  breqd  5085  poeq1  5502  soeq1  5520  freq1  5555  fveq1  6766  foeqcnvco  7165  f1eqcocnv  7166  f1eqcocnvOLD  7167  isoeq2  7182  isoeq3  7183  brfvopab  7323  ofreq  7528  supeq3  9196  oieq1  9259  ttrcleq  9455  dcomex  10191  axdc2lem  10192  brdom3  10272  brdom7disj  10275  brdom6disj  10276  dfrtrclrec2  14757  relexpindlem  14762  rtrclind  14764  shftfval  14769  isprs  18003  isdrs  18007  ispos  18020  istos  18124  efglem  19310  frgpuplem  19366  ordtval  22328  utop2nei  23390  utop3cls  23391  isucn2  23419  ucnima  23421  iducn  23423  ex-opab  28782  resspos  31230  acycgr0v  33096  prclisacycgr  33099  satf  33301  eqfunresadj  33721  cureq  35739  poimirlem31  35794  poimir  35796  cosseq  36535  elrefrels3  36622  elcnvrefrels3  36635  elsymrels3  36654  elsymrels5  36656  eltrrels3  36680  eleqvrels3  36692  brabsb2  36862  rfovfvd  41569  fsovrfovd  41576  sprsymrelf  44903  sprsymrelfo  44905  upwlkbprop  45256