Theorem breq1i 5099

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
breq1i	⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq1 5095	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  eqbrtri  5113  brtpos0  8166  brtpos  8168  euen1  8952  euen1b  8953  2dom  8955  0sdom1domALT  9136  1sdom2  9137  modom2  9141  infglb  9381  infglbb  9382  cnfcom3lem  9599  axdclem2  10414  rnct  10419  cfpwsdom  10478  inar1  10669  reclem3pr  10943  gt0srpr  10972  mappsrpr  11002  ltpsrpr  11003  map2psrpr  11004  axpre-mulgt0  11062  lt0neg1  11626  le0neg1  11628  reclt1  12020  addltmul  12360  eluz2b1  12820  xlt0neg1  13121  xle0neg1  13123  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  elfznelfzo  13675  bernneq  14136  nn0opthlem1  14175  faclbnd4lem1  14200  hashge0  14294  hashgt23el  14331  hashge2el2difr  14388  cbvsum  15602  divcnvshft  15762  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  iprodmul  15910  oddge22np1  16260  nn0o1gt2  16292  divalglem1  16305  divalglem6  16309  isprm3  16594  dvdsnprmd  16601  2mulprm  16604  ge2nprmge4  16612  prmgaplem3  16965  isnzr2  20403  chrdvds  21433  chrcong  21434  lindsmm  21735  cpmidpmat  22758  csdfil  23779  iscau3  25176  ioombl1lem4  25460  itg2cn  25662  radcnvlt1  26325  sincosq1sgn  26405  sincosq3sgn  26407  sincosq4sgn  26408  ang180lem3  26719  leibpilem2  26849  issqf  27044  bposlem6  27198  gausslemma2dlem3  27277  nosupinfsep  27642  addscut  27890  mulscut  28040  mulscan2d  28087  recsex  28126  abssneg  28154  avgslt1d  28344  avgslt2d  28345  clwlkclwwlklem2  29944  clwlkclwwlk2  29947  clwlkclwwlkf  29952  clwlknf1oclwwlknlem1  30025  konigsberglem5  30200  cvexchi  32313  addltmulALT  32390  xnn01gt  32714  dya2iocct  34254  ballotlemi1  34477  signswch  34535  usgrgt2cycl  35113  cusgracyclt3v  35139  sumeq2si  36186  prodeq2si  36188  cbvprodvw2  36231  cos2h  37601  tan2h  37602  lhpocnel2  40008  cdlemk19w  40961  lcmineqlem  42035  rencldnfilem  42803  imsqrtvalex  43629  frege70  43916  frege118  43964  hashnzfzclim  44305  dvradcnv2  44330  binomcxplemnotnn0  44339  supxrleubrnmptf  45440  ioonct  45528  fourierdlem112  46209  salexct2  46330  addmodne  47338  m1modnep2mod  47346  difmodm1lt  47353  flsqrt5  47588  lighneallem4b  47603  fpprel2  47735  gbegt5  47755  gbowgt5  47756  gbowge7  47757  gbege6  47759  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbalt  47775  sbgoldbm  47778  nnsum3primesle9  47788  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  tgblthelfgott  47809  gpg3kgrtriexlem5  48081