Theorem breqi 5112

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 5108	. 2 ⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-br 5107

This theorem is used by:  f1ompt  7132  isocnv3  7360  eqfunresadj  7390  brtpos2  8274  brwitnlem  8540  brdifun  8773  omxpenlem  9122  infxpenlem  10116  ltpiord  10996  nqerf  11039  nqerid  11042  ordpinq  11052  ltxrlt  11404  ltxr  13268  trclublem  15174  oduleg  18490  oduposb  18527  join0  18603  meet0  18604  xmeterval  24778  pi1cpbl  25392  lenlts  28136  ltgov  29087  brbtwn  29504  avril1  31091  axhcompl-zf  31627  hlimadd  31822  hhcmpl  31829  hhcms  31832  hlim0  31864  leacgra  33091  tgextalt1  33103  tgextalt2  33104  fcoinvbr  33268  brprop  33358  posrasymb  33595  trleile  33599  isarchi  33810  pstmfval  34595  pstmxmet  34596  lmlim  34646  morleylemrneab  35367  rankse  35822  fineqvnttrclse  35891  satfbrsuc  36297  brtxp  36819  brpprod  36824  brpprod3b  36826  brtxpsd2  36834  brdomain  36872  brrange  36873  brimg  36876  brapply  36877  brsuccf  36881  brrestrict  36890  brub  36895  brlb  36896  colineardim1  37003  broutsideof  37063  fneval  37317  relowlpssretop  38478  phpreu  38718  poimirlem26  38755  br1cnvres  39397  brid  39435  eqres  39463  alrmomorn  39481  brabidgaw  39496  brabidga  39497  brxrn  39506  br1cossinres  39660  br1cossxrnres  39661  brnonrel  44779  brcofffn  45221  brco2f1o  45222  brco3f1o  45223  clsneikex  45296  clsneinex  45297  clsneiel1  45298  neicvgmex  45307  neicvgel1  45309  brpermmodel  46186  climreeq  46828  xlimres  47034  xlimcl  47035  xlimclim  47037  xlimconst  47038  xlimbr  47040  xlimmnfvlem1  47045  xlimmnfvlem2  47046  xlimpnfvlem1  47049  xlimpnfvlem2  47050  xlimuni  47066  lambert0  48140  lamberte  48141  islmd  51051  iscmd  51052  lmdran  51057  cmdlan  51058  gte-lte  51095  gt-lt  51096  gte-lteh  51097  gt-lth  51098