Theorem breq 5077

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  ⟨cop 4568   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-br 5076

This theorem is referenced by:  breqi  5081  breqd  5086  poeq1  5507  soeq1  5525  freq1  5560  fveq1  6782  foeqcnvco  7181  f1eqcocnv  7182  f1eqcocnvOLD  7183  isoeq2  7198  isoeq3  7199  brfvopab  7341  ofreq  7546  supeq3  9217  oieq1  9280  ttrcleq  9476  dcomex  10212  axdc2lem  10213  brdom3  10293  brdom7disj  10296  brdom6disj  10297  dfrtrclrec2  14778  relexpindlem  14783  rtrclind  14785  shftfval  14790  isprs  18024  isdrs  18028  ispos  18041  istos  18145  efglem  19331  frgpuplem  19387  ordtval  22349  utop2nei  23411  utop3cls  23412  isucn2  23440  ucnima  23442  iducn  23444  ex-opab  28805  resspos  31253  acycgr0v  33119  prclisacycgr  33122  satf  33324  eqfunresadj  33744  cureq  35762  poimirlem31  35817  poimir  35819  cosseq  36556  elrefrels3  36643  elcnvrefrels3  36656  elsymrels3  36675  elsymrels5  36677  eltrrels3  36701  eleqvrels3  36713  brabsb2  36883  rfovfvd  41617  fsovrfovd  41624  sprsymrelf  44958  sprsymrelfo  44960  upwlkbprop  45311