Theorem breq 5151

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ⟨cop 4635   class class class wbr 5149

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-br 5150

This theorem is referenced by:  breqi  5155  breqd  5160  poeq1  5592  soeq1  5610  freq1  5647  fveq1  6891  foeqcnvco  7298  f1eqcocnv  7299  f1eqcocnvOLD  7300  isoeq2  7315  isoeq3  7316  eqfunresadj  7357  brfvopab  7466  ofreq  7674  supeq3  9444  oieq1  9507  ttrcleq  9704  dcomex  10442  axdc2lem  10443  brdom3  10523  brdom7disj  10526  brdom6disj  10527  dfrtrclrec2  15005  relexpindlem  15010  rtrclind  15012  shftfval  15017  isprs  18250  isdrs  18254  ispos  18267  istos  18371  efglem  19584  frgpuplem  19640  ordtval  22693  utop2nei  23755  utop3cls  23756  isucn2  23784  ucnima  23786  iducn  23788  ex-opab  29685  resspos  32136  acycgr0v  34139  prclisacycgr  34142  satf  34344  cureq  36464  poimirlem31  36519  poimir  36521  cosseq  37296  elrefrels3  37389  elcnvrefrels3  37405  elsymrels3  37424  elsymrels5  37426  eltrrels3  37450  eleqvrels3  37463  brabsb2  37732  rfovfvd  42753  fsovrfovd  42760  sprsymrelf  46163  sprsymrelfo  46165  upwlkbprop  46516