Theorem breq 5068

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-br 5067

This theorem is referenced by:  breqi  5072  breqd  5077  poeq1  5477  soeq1  5494  freq1  5525  fveq1  6669  foeqcnvco  7056  f1eqcocnv  7057  isoeq2  7071  isoeq3  7072  brfvopab  7211  ofreq  7412  supeq3  8913  oieq1  8976  dcomex  9869  axdc2lem  9870  brdom3  9950  brdom7disj  9953  brdom6disj  9954  dfrtrclrec2  14416  relexpindlem  14422  rtrclind  14424  shftfval  14429  isprs  17540  isdrs  17544  ispos  17557  istos  17645  efglem  18842  frgpuplem  18898  ordtval  21797  utop2nei  22859  utop3cls  22860  isucn2  22888  ucnima  22890  iducn  22892  ex-opab  28211  resspos  30646  acycgr0v  32395  prclisacycgr  32398  satf  32600  eqfunresadj  33004  cureq  34883  poimirlem31  34938  poimir  34940  cosseq  35686  elrefrels3  35773  elcnvrefrels3  35786  elsymrels3  35805  elsymrels5  35807  eltrrels3  35831  eleqvrels3  35843  brabsb2  36013  rfovfvd  40368  fsovrfovd  40375  sprsymrelf  43677  sprsymrelfo  43679  upwlkbprop  44033