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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ⟨cop 4564   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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-br 5076

This theorem is referenced by:  breqi  5081  breqd  5086  poeq1  5532  soeq1  5550  freq1  5588  fveq1  6830  foeqcnvco  7248  f1eqcocnv  7249  isoeq2  7266  isoeq3  7267  eqfunresadj  7308  brfvopab  7417  ofreq  7628  supeq3  9356  oieq1  9421  ttrcleq  9625  dcomex  10364  axdc2lem  10365  brdom3  10445  brdom7disj  10448  brdom6disj  10449  dfrtrclrec2  15015  relexpindlem  15020  rtrclind  15022  shftfval  15027  isprs  18257  isdrs  18262  ispos  18275  istos  18377  resspos  18390  chneq1  18573  efglem  19686  frgpuplem  19742  ordtval  23176  utop2nei  24237  utop3cls  24238  isucn2  24265  ucnima  24267  iducn  24269  ex-opab  30524  acycgr0v  35391  prclisacycgr  35394  satf  35596  cureq  37978  poimirlem31  38033  poimir  38035  cosseq  38898  elrefrels3  38981  elcnvrefrels3  38997  elsymrels3  39020  elsymrels5  39022  eltrrels3  39046  eleqvrels3  39059  brabsb2  39369  rfovfvd  44461  fsovrfovd  44468  relpeq2  45404  relpeq3  45405  sprsymrelf  47984  sprsymrelfo  47986  upwlkbprop  48643