Theorem breq 5041

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  ⟨cop 4533   class class class wbr 5039

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 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809  df-br 5040

This theorem is referenced by:  breqi  5045  breqd  5050  poeq1  5456  soeq1  5474  freq1  5506  fveq1  6694  foeqcnvco  7088  f1eqcocnv  7089  f1eqcocnvOLD  7090  isoeq2  7105  isoeq3  7106  brfvopab  7246  ofreq  7450  supeq3  9043  oieq1  9106  dcomex  10026  axdc2lem  10027  brdom3  10107  brdom7disj  10110  brdom6disj  10111  dfrtrclrec2  14586  relexpindlem  14591  rtrclind  14593  shftfval  14598  isprs  17758  isdrs  17762  ispos  17775  istos  17878  efglem  19060  frgpuplem  19116  ordtval  22040  utop2nei  23102  utop3cls  23103  isucn2  23130  ucnima  23132  iducn  23134  ex-opab  28469  resspos  30917  acycgr0v  32777  prclisacycgr  32780  satf  32982  eqfunresadj  33405  cureq  35439  poimirlem31  35494  poimir  35496  cosseq  36235  elrefrels3  36322  elcnvrefrels3  36335  elsymrels3  36354  elsymrels5  36356  eltrrels3  36380  eleqvrels3  36392  brabsb2  36562  rfovfvd  41228  fsovrfovd  41235  sprsymrelf  44563  sprsymrelfo  44565  upwlkbprop  44916