Theorem breq 5113

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ⟨cop 4598   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-br 5112

This theorem is referenced by:  breqi  5117  breqd  5122  poeq1  5573  soeq1  5591  freq1  5629  fveq1  6881  foeqcnvco  7299  f1eqcocnv  7300  isoeq2  7317  isoeq3  7318  eqfunresadj  7359  brfvopab  7468  ofreq  7679  supeq3  9409  oieq1  9474  ttrcleq  9678  dcomex  10431  axdc2lem  10432  brdom3  10512  brdom7disj  10515  brdom6disj  10516  dfrtrclrec2  15095  relexpindlem  15100  rtrclind  15102  shftfval  15107  isprs  18352  isdrs  18357  ispos  18370  istos  18472  resspos  18485  chneq1  18668  efglem  19786  frgpuplem  19842  ordtval  23315  utop2nei  24376  utop3cls  24377  isucn2  24404  ucnima  24406  iducn  24408  ex-opab  30724  acycgr0v  35573  prclisacycgr  35576  satf  35778  cureq  38170  poimirlem31  38225  poimir  38227  cosseq  39090  elrefrels3  39173  elcnvrefrels3  39189  elsymrels3  39212  elsymrels5  39214  eltrrels3  39238  eleqvrels3  39251  brabsb2  39561  rfovfvd  44655  fsovrfovd  44662  relpeq2  45581  relpeq3  45582  sprsymrelf  48168  sprsymrelfo  48170  upwlkbprop  48827