Theorem breq1i 5131

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  eqbrtri  5145  brtpos0  8237  brtpos  8239  euen1  9046  euen1b  9047  2dom  9049  0sdom1domALT  9252  1sdom2  9253  modom2  9258  1sdomOLD  9262  infglb  9508  infglbb  9509  cnfcom3lem  9722  pr2nelemOLD  10022  axdclem2  10539  rnct  10544  cfpwsdom  10603  inar1  10794  reclem3pr  11068  gt0srpr  11097  mappsrpr  11127  ltpsrpr  11128  map2psrpr  11129  axpre-mulgt0  11187  lt0neg1  11748  le0neg1  11750  reclt1  12142  addltmul  12482  eluz2b1  12940  xlt0neg1  13240  xle0neg1  13242  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  elfznelfzo  13793  bernneq  14252  nn0opthlem1  14291  faclbnd4lem1  14316  hashge0  14410  hashgt23el  14447  hashge2el2difr  14504  cbvsum  15716  divcnvshft  15876  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  iprodmul  16024  oddge22np1  16373  nn0o1gt2  16405  divalglem1  16418  divalglem6  16422  isprm3  16707  dvdsnprmd  16714  2mulprm  16717  ge2nprmge4  16725  prmgaplem3  17078  isnzr2  20483  chrdvds  21492  chrcong  21493  lindsmm  21793  cpmidpmat  22816  csdfil  23837  iscau3  25235  ioombl1lem4  25519  itg2cn  25721  radcnvlt1  26384  sincosq1sgn  26464  sincosq3sgn  26466  sincosq4sgn  26467  ang180lem3  26778  leibpilem2  26908  issqf  27103  bposlem6  27257  gausslemma2dlem3  27336  nosupinfsep  27701  addscut  27942  mulscut  28092  mulscan2d  28139  recsex  28178  abssneg  28206  clwlkclwwlklem2  29986  clwlkclwwlk2  29989  clwlkclwwlkf  29994  clwlknf1oclwwlknlem1  30067  konigsberglem5  30242  cvexchi  32355  addltmulALT  32432  xnn01gt  32752  dya2iocct  34317  ballotlemi1  34540  signswch  34598  usgrgt2cycl  35157  cusgracyclt3v  35183  sumeq2si  36225  prodeq2si  36227  cbvprodvw2  36270  cos2h  37640  tan2h  37641  lhpocnel2  40043  cdlemk19w  40996  lcmineqlem  42070  rencldnfilem  42818  imsqrtvalex  43645  frege70  43932  frege118  43980  hashnzfzclim  44321  dvradcnv2  44346  binomcxplemnotnn0  44355  supxrleubrnmptf  45458  ioonct  45546  fourierdlem112  46227  salexct2  46348  addmodne  47353  m1modnep2mod  47361  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  48069  difmodm1lt  48482