Theorem breq1i 4590

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

Syntax hints:   ↔ wb 195   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  eqbrtri  4604  brtpos0  7246  brtpos  7248  euen1  7912  euen1b  7913  2dom  7915  0sdom1dom  8043  modom2  8047  1sdom  8048  infglb  8279  infglbb  8280  cnfcom3lem  8483  pr2nelem  8710  axdclem2  9225  cfpwsdom  9285  inar1  9476  reclem3pr  9750  gt0srpr  9778  mappsrpr  9808  ltpsrpr  9809  map2psrpr  9810  axpre-mulgt0  9868  lt0neg1  10413  le0neg1  10415  reclt1  10797  addltmul  11145  eluz2b1  11635  xlt0neg1  11924  xle0neg1  11926  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  elfznelfzo  12439  bernneq  12852  nn0opthlem1  12917  faclbnd4lem1  12942  hashge0  13037  hashge2el2difr  13118  cbvsum  14273  divcnvshft  14426  cbvprod  14484  iprodmul  14573  oddge22np1  14911  nn0o1gt2  14935  divalglem1  14955  divalglem6  14959  isprm2lem  15232  isprm3  15234  dvdsnprmd  15241  prmgaplem3  15595  isnzr2  19084  chrdvds  19695  chrcong  19696  lindsmm  19986  cpmidpmat  20497  csdfil  21508  iscau3  22884  ioombl1lem4  23136  itg2cn  23336  radcnvlt1  23976  sincosq1sgn  24054  sincosq3sgn  24056  sincosq4sgn  24057  ang180lem3  24341  leibpilem2  24468  issqf  24662  bposlem6  24814  gausslemma2dlem3  24893  clwlkisclwwlklem1  26315  frgra3v  26529  3vfriswmgra  26532  numclwwlkovf2ex  26613  cvexchi  28612  addltmulALT  28689  rnct  28879  dya2iocct  29669  ballotlemi1  29891  signswch  29964  cos2h  32570  tan2h  32571  lhpocnel2  34323  cdlemk19w  35278  rencldnfilem  36402  frege70  37247  frege118  37295  hashnzfzclim  37543  dvradcnv2  37568  binomcxplemnotnn0  37577  ioonct  38611  fourierdlem112  39111  salexct2  39233  flsqrt5  40047  lighneallem4b  40064  gbegt5  40183  gbogt5  40184  gboge7  40185  gbege6  40187  bgoldbwt  40199  bgoldbst  40200  sgoldbalt  40203  nnsum3primesle9  40210  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  tgblthelfgott  40229  tgblthelfgottOLD  40236  clwlkclwwlklem2  41209  konigsberglem5  41426  av-numclwwlkovf2ex  41517  difmodm1lt  42111