Theorem breq 5091

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ⟨cop 4579   class class class wbr 5089

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-br 5090

This theorem is referenced by:  breqi  5095  breqd  5100  poeq1  5525  soeq1  5543  freq1  5581  fveq1  6821  foeqcnvco  7234  f1eqcocnv  7235  isoeq2  7252  isoeq3  7253  eqfunresadj  7294  brfvopab  7403  ofreq  7614  supeq3  9333  oieq1  9398  ttrcleq  9599  dcomex  10338  axdc2lem  10339  brdom3  10419  brdom7disj  10422  brdom6disj  10423  dfrtrclrec2  14965  relexpindlem  14970  rtrclind  14972  shftfval  14977  isprs  18202  isdrs  18207  ispos  18220  istos  18322  resspos  18335  chneq1  18518  efglem  19628  frgpuplem  19684  ordtval  23104  utop2nei  24165  utop3cls  24166  isucn2  24193  ucnima  24195  iducn  24197  ex-opab  30412  acycgr0v  35192  prclisacycgr  35195  satf  35397  cureq  37635  poimirlem31  37690  poimir  37692  cosseq  38527  elrefrels3  38610  elcnvrefrels3  38626  elsymrels3  38649  elsymrels5  38651  eltrrels3  38675  eleqvrels3  38688  brabsb2  38960  rfovfvd  44094  fsovrfovd  44101  relpeq2  45037  relpeq3  45038  sprsymrelf  47594  sprsymrelfo  47596  upwlkbprop  48237