Theorem breq 5168

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ⟨cop 4654   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-br 5167

This theorem is referenced by:  breqi  5172  breqd  5177  poeq1  5610  soeq1  5629  freq1  5667  fveq1  6919  foeqcnvco  7336  f1eqcocnv  7337  isoeq2  7354  isoeq3  7355  eqfunresadj  7396  brfvopab  7507  ofreq  7718  supeq3  9518  oieq1  9581  ttrcleq  9778  dcomex  10516  axdc2lem  10517  brdom3  10597  brdom7disj  10600  brdom6disj  10601  dfrtrclrec2  15107  relexpindlem  15112  rtrclind  15114  shftfval  15119  isprs  18367  isdrs  18371  ispos  18384  istos  18488  efglem  19758  frgpuplem  19814  ordtval  23218  utop2nei  24280  utop3cls  24281  isucn2  24309  ucnima  24311  iducn  24313  ex-opab  30464  resspos  32939  acycgr0v  35116  prclisacycgr  35119  satf  35321  cureq  37556  poimirlem31  37611  poimir  37613  cosseq  38382  elrefrels3  38475  elcnvrefrels3  38491  elsymrels3  38510  elsymrels5  38512  eltrrels3  38536  eleqvrels3  38549  brabsb2  38818  rfovfvd  43964  fsovrfovd  43971  sprsymrelf  47369  sprsymrelfo  47371  upwlkbprop  47861