Theorem breq 5104

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  ⟨cop 4590   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839  df-br 5103

This theorem is referenced by:  breqi  5108  breqd  5113  poeq1  5560  soeq1  5578  freq1  5616  fveq1  6868  foeqcnvco  7286  f1eqcocnv  7287  isoeq2  7304  isoeq3  7305  eqfunresadj  7346  brfvopab  7455  ofreq  7666  supeq3  9397  oieq1  9462  ttrcleq  9666  dcomex  10406  axdc2lem  10407  brdom3  10487  brdom7disj  10490  brdom6disj  10491  dfrtrclrec2  15073  relexpindlem  15078  rtrclind  15080  shftfval  15085  isprs  18330  isdrs  18335  ispos  18348  istos  18450  resspos  18463  chneq1  18646  efglem  19758  frgpuplem  19814  ordtval  23251  utop2nei  24312  utop3cls  24313  isucn2  24340  ucnima  24342  iducn  24344  ex-opab  30636  acycgr0v  35503  prclisacycgr  35506  satf  35708  cureq  38100  poimirlem31  38155  poimir  38157  cosseq  39020  elrefrels3  39103  elcnvrefrels3  39119  elsymrels3  39142  elsymrels5  39144  eltrrels3  39168  eleqvrels3  39181  brabsb2  39491  rfovfvd  44583  fsovrfovd  44590  relpeq2  45526  relpeq3  45527  sprsymrelf  48106  sprsymrelfo  48108  upwlkbprop  48765