Theorem breq 5108

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ⟨cop 4838   class class class wbr 5106

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-br 5107

This theorem is used by:  breqi  5112  breqd  5117  poeq1  5566  soeq1  5584  freq1  5622  fveq1  6904  foeqcnvco  7328  f1eqcocnv  7329  isoeq2  7346  isoeq3  7347  eqfunresadj  7390  brfvopab  7497  ofreq  7718  cureq  8914  supeq3  9465  oieq1  9530  ttrcleq  9734  dcomex  10549  axdc2lem  10550  brdom3  10631  brdom7disj  10634  brdom6disj  10635  dfrtrclrec2  15237  relexpindlem  15242  rtrclind  15244  shftfval  15249  isprs  18496  isdrs  18501  ispos  18514  istos  18616  resspos  18629  chneq1  18812  efglem  19957  frgpuplem  20013  ordtval  23534  utop2nei  24596  utop3cls  24597  isucn2  24624  ucnima  24626  iducn  24628  ex-opab  31060  acycgr0v  36069  prclisacycgr  36072  satf  36284  poimirlem31  38760  poimir  38762  cosseq  39639  elrefrels3  39722  elcnvrefrels3  39738  elsymrels3  39761  elsymrels5  39763  eltrrels3  39787  eleqvrels3  39800  brabsb2  40110  rfovfvd  45192  fsovrfovd  45199  relpeq2  46128  relpeq3  46129  sprsymrelf  48780  sprsymrelfo  48782  upwlkbprop  49439