Theorem breq 5104

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ⟨cop 4589   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-br 5103

This theorem is used by:  breqi  5108  breqd  5113  poeq1  5561  soeq1  5579  freq1  5617  fveq1  6884  foeqcnvco  7308  f1eqcocnv  7309  isoeq2  7326  isoeq3  7327  eqfunresadj  7370  brfvopab  7477  ofreq  7697  cureq  8889  supeq3  9441  oieq1  9506  ttrcleq  9710  dcomex  10525  axdc2lem  10526  brdom3  10607  brdom7disj  10610  brdom6disj  10611  dfrtrclrec2  15211  relexpindlem  15216  rtrclind  15218  shftfval  15223  isprs  18470  isdrs  18475  ispos  18488  istos  18590  resspos  18603  chneq1  18786  efglem  19930  frgpuplem  19986  ordtval  23507  utop2nei  24569  utop3cls  24570  isucn2  24597  ucnima  24599  iducn  24601  ex-opab  31033  acycgr0v  35913  prclisacycgr  35916  satf  36118  poimirlem31  38570  poimir  38572  cosseq  39449  elrefrels3  39532  elcnvrefrels3  39548  elsymrels3  39571  elsymrels5  39573  eltrrels3  39597  eleqvrels3  39610  brabsb2  39920  rfovfvd  45002  fsovrfovd  45009  relpeq2  45935  relpeq3  45936  sprsymrelf  48577  sprsymrelfo  48579  upwlkbprop  49236