Theorem breq 5088

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-br 5087

This theorem is referenced by:  breqi  5092  breqd  5097  poeq1  5537  soeq1  5555  freq1  5593  fveq1  6835  foeqcnvco  7250  f1eqcocnv  7251  isoeq2  7268  isoeq3  7269  eqfunresadj  7310  brfvopab  7419  ofreq  7630  supeq3  9357  oieq1  9422  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  23168  utop2nei  24229  utop3cls  24230  isucn2  24257  ucnima  24259  iducn  24261  ex-opab  30521  acycgr0v  35350  prclisacycgr  35353  satf  35555  cureq  37937  poimirlem31  37992  poimir  37994  cosseq  38857  elrefrels3  38940  elcnvrefrels3  38956  elsymrels3  38979  elsymrels5  38981  eltrrels3  39005  eleqvrels3  39018  brabsb2  39328  rfovfvd  44453  fsovrfovd  44460  relpeq2  45396  relpeq3  45397  sprsymrelf  47973  sprsymrelfo  47975  upwlkbprop  48632