Theorem breq 5116

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ⟨cop 4600   class class class wbr 5114

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-br 5115

This theorem is used by:  breqi  5120  breqd  5125  poeq1  5577  soeq1  5595  freq1  5633  fveq1  6887  foeqcnvco  7309  f1eqcocnv  7310  isoeq2  7327  isoeq3  7328  eqfunresadj  7371  brfvopab  7480  ofreq  7691  supeq3  9419  oieq1  9484  ttrcleq  9688  dcomex  10449  axdc2lem  10450  brdom3  10530  brdom7disj  10533  brdom6disj  10534  dfrtrclrec2  15121  relexpindlem  15126  rtrclind  15128  shftfval  15133  isprs  18377  isdrs  18382  ispos  18395  istos  18497  resspos  18510  chneq1  18693  efglem  19811  frgpuplem  19867  ordtval  23376  utop2nei  24437  utop3cls  24438  isucn2  24465  ucnima  24467  iducn  24469  ex-opab  30813  acycgr0v  35653  prclisacycgr  35656  satf  35858  cureq  38280  poimirlem31  38335  poimir  38337  cosseq  39198  elrefrels3  39281  elcnvrefrels3  39297  elsymrels3  39320  elsymrels5  39322  eltrrels3  39346  eleqvrels3  39359  brabsb2  39669  rfovfvd  44761  fsovrfovd  44768  relpeq2  45687  relpeq3  45688  sprsymrelf  48277  sprsymrelfo  48279  upwlkbprop  48936