Theorem breqi 5080

Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)

Hypothesis

Ref	Expression
breqi.1	⊢ 𝑅 = 𝑆

Assertion

Ref	Expression
breqi	⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)

Proof of Theorem breqi

Step	Hyp	Ref	Expression
1		breqi.1	. 2 ⊢ 𝑅 = 𝑆
2		breq 5076	. 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-br 5075

This theorem is referenced by:  f1ompt  7052  isocnv3  7276  eqfunresadj  7304  brtpos2  8171  brwitnlem  8431  brdifun  8663  omxpenlem  9005  infxpenlem  9924  ltpiord  10799  nqerf  10842  nqerid  10845  ordpinq  10855  ltxrlt  11205  ltxr  13055  trclublem  14946  oduleg  18245  oduposb  18282  join0  18358  meet0  18359  xmeterval  24385  pi1cpbl  24999  lenlts  27704  ltgov  28653  brbtwn  28956  avril1  30521  axhcompl-zf  31057  hlimadd  31252  hhcmpl  31259  hhcms  31262  hlim0  31294  fcoinvbr  32663  brprop  32758  posrasymb  33015  trleile  33019  isarchi  33231  pstmfval  34028  pstmxmet  34029  lmlim  34079  fineqvnttrclse  35256  satfbrsuc  35536  brtxp  36048  brpprod  36053  brpprod3b  36055  brtxpsd2  36063  brdomain  36101  brrange  36102  brimg  36105  brapply  36106  brsuccf  36110  brrestrict  36119  brub  36124  brlb  36125  colineardim1  36231  broutsideof  36291  fneval  36522  relowlpssretop  37668  phpreu  37913  poimirlem26  37955  br1cnvres  38583  brid  38621  eqres  38649  alrmomorn  38667  brabidgaw  38682  brabidga  38683  brxrn  38692  br1cossinres  38846  br1cossxrnres  38847  brnonrel  44004  brcofffn  44446  brco2f1o  44447  brco3f1o  44448  clsneikex  44521  clsneinex  44522  clsneiel1  44523  neicvgmex  44532  neicvgel1  44534  brpermmodel  45418  climreeq  46031  xlimres  46237  xlimcl  46238  xlimclim  46240  xlimconst  46241  xlimbr  46243  xlimmnfvlem1  46248  xlimmnfvlem2  46249  xlimpnfvlem1  46252  xlimpnfvlem2  46253  xlimuni  46269  lambert0  47323  lamberte  47324  islmd  50128  iscmd  50129  lmdran  50134  cmdlan  50135  gte-lte  50187  gt-lt  50188  gte-lteh  50189  gt-lth  50190