Theorem breq 5109

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-br 5108

This theorem is used by:  breqi  5113  breqd  5118  poeq1  5570  soeq1  5588  freq1  5626  fveq1  6881  foeqcnvco  7304  f1eqcocnv  7305  isoeq2  7322  isoeq3  7323  eqfunresadj  7366  brfvopab  7473  ofreq  7685  cureq  8871  supeq3  9422  oieq1  9487  ttrcleq  9691  dcomex  10452  axdc2lem  10453  brdom3  10534  brdom7disj  10537  brdom6disj  10538  dfrtrclrec2  15133  relexpindlem  15138  rtrclind  15140  shftfval  15145  isprs  18388  isdrs  18393  ispos  18406  istos  18508  resspos  18521  chneq1  18704  efglem  19844  frgpuplem  19900  ordtval  23415  utop2nei  24477  utop3cls  24478  isucn2  24505  ucnima  24507  iducn  24509  ex-opab  30898  acycgr0v  35714  prclisacycgr  35717  satf  35919  poimirlem31  38387  poimir  38389  cosseq  39251  elrefrels3  39334  elcnvrefrels3  39350  elsymrels3  39373  elsymrels5  39375  eltrrels3  39399  eleqvrels3  39412  brabsb2  39722  rfovfvd  44829  fsovrfovd  44836  relpeq2  45755  relpeq3  45756  sprsymrelf  48382  sprsymrelfo  48384  upwlkbprop  49041