Theorem breq1i 5149

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

Syntax hints:   ↔ wb 206   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  eqbrtri  5163  brtpos0  8259  brtpos  8261  euen1  9068  euen1b  9069  2dom  9071  0sdom1domALT  9276  1sdom2  9277  modom2  9282  1sdomOLD  9286  infglb  9531  infglbb  9532  cnfcom3lem  9744  pr2nelemOLD  10044  axdclem2  10561  rnct  10566  cfpwsdom  10625  inar1  10816  reclem3pr  11090  gt0srpr  11119  mappsrpr  11149  ltpsrpr  11150  map2psrpr  11151  axpre-mulgt0  11209  lt0neg1  11770  le0neg1  11772  reclt1  12164  addltmul  12504  eluz2b1  12962  xlt0neg1  13262  xle0neg1  13264  iccshftr  13527  iccshftl  13529  iccdil  13531  icccntr  13533  elfznelfzo  13812  bernneq  14269  nn0opthlem1  14308  faclbnd4lem1  14333  hashge0  14427  hashgt23el  14464  hashge2el2difr  14521  cbvsum  15732  divcnvshft  15892  cbvprod  15950  cbvprodv  15951  prodeq1i  15953  iprodmul  16040  oddge22np1  16387  nn0o1gt2  16419  divalglem1  16432  divalglem6  16436  isprm3  16721  dvdsnprmd  16728  2mulprm  16731  ge2nprmge4  16739  prmgaplem3  17092  isnzr2  20519  chrdvds  21542  chrcong  21543  lindsmm  21849  cpmidpmat  22880  csdfil  23903  iscau3  25313  ioombl1lem4  25597  itg2cn  25799  radcnvlt1  26462  sincosq1sgn  26541  sincosq3sgn  26543  sincosq4sgn  26544  ang180lem3  26855  leibpilem2  26985  issqf  27180  bposlem6  27334  gausslemma2dlem3  27413  nosupinfsep  27778  addscut  28012  mulscut  28159  mulscan2d  28206  recsex  28244  abssneg  28272  clwlkclwwlklem2  30020  clwlkclwwlk2  30023  clwlkclwwlkf  30028  clwlknf1oclwwlknlem1  30101  konigsberglem5  30276  cvexchi  32389  addltmulALT  32466  xnn01gt  32775  dya2iocct  34283  ballotlemi1  34506  signswch  34577  usgrgt2cycl  35136  cusgracyclt3v  35162  sumeq2si  36204  prodeq2si  36206  cbvprodvw2  36249  cos2h  37619  tan2h  37620  lhpocnel2  40022  cdlemk19w  40975  lcmineqlem  42054  rencldnfilem  42836  imsqrtvalex  43664  frege70  43951  frege118  43999  hashnzfzclim  44346  dvradcnv2  44371  binomcxplemnotnn0  44380  supxrleubrnmptf  45467  ioonct  45555  fourierdlem112  46238  salexct2  46359  addmodne  47351  m1modnep2mod  47359  flsqrt5  47586  lighneallem4b  47601  fpprel2  47733  gbegt5  47753  gbowgt5  47754  gbowge7  47755  gbege6  47757  sbgoldbwt  47769  sbgoldbst  47770  sbgoldbalt  47773  sbgoldbm  47776  nnsum3primesle9  47786  nnsum4primesevenALTV  47793  bgoldbtbndlem1  47797  tgblthelfgott  47807  gpg3kgrtriexlem5  48048  difmodm1lt  48448