Theorem breq 5105

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  breqi  5109  breqd  5114  poeq1  5559  soeq1  5577  freq1  5615  fveq1  6873  foeqcnvco  7297  f1eqcocnv  7298  isoeq2  7315  isoeq3  7316  eqfunresadj  7359  brfvopab  7466  ofreq  7681  cureq  8868  supeq3  9419  oieq1  9484  ttrcleq  9688  dcomex  10482  axdc2lem  10483  brdom3  10564  brdom7disj  10567  brdom6disj  10568  dfrtrclrec2  15164  relexpindlem  15169  rtrclind  15171  shftfval  15176  isprs  18417  isdrs  18422  ispos  18435  istos  18537  resspos  18550  chneq1  18733  efglem  19877  frgpuplem  19933  ordtval  23454  utop2nei  24516  utop3cls  24517  isucn2  24544  ucnima  24546  iducn  24548  ex-opab  30952  acycgr0v  35828  prclisacycgr  35831  satf  36033  poimirlem31  38483  poimir  38485  cosseq  39362  elrefrels3  39445  elcnvrefrels3  39461  elsymrels3  39484  elsymrels5  39486  eltrrels3  39510  eleqvrels3  39523  brabsb2  39833  rfovfvd  44940  fsovrfovd  44947  relpeq2  45866  relpeq3  45867  sprsymrelf  48493  sprsymrelfo  48495  upwlkbprop  49152