Theorem breq1i 5077

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

Syntax hints:   ↔ wb 205   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  eqbrtri  5091  brtpos0  8020  brtpos  8022  euen1  8770  euen1b  8771  2dom  8774  0sdom1dom  8950  modom2  8954  1sdom  8955  infglb  9179  infglbb  9180  cnfcom3lem  9391  pr2nelem  9691  axdclem2  10207  rnct  10212  cfpwsdom  10271  inar1  10462  reclem3pr  10736  gt0srpr  10765  mappsrpr  10795  ltpsrpr  10796  map2psrpr  10797  axpre-mulgt0  10855  lt0neg1  11411  le0neg1  11413  reclt1  11800  addltmul  12139  eluz2b1  12588  xlt0neg1  12882  xle0neg1  12884  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  elfznelfzo  13420  bernneq  13872  nn0opthlem1  13910  faclbnd4lem1  13935  hashge0  14030  hashgt23el  14067  hashge2el2difr  14123  cbvsum  15335  divcnvshft  15495  cbvprod  15553  iprodmul  15641  oddge22np1  15986  nn0o1gt2  16018  divalglem1  16031  divalglem6  16035  isprm3  16316  dvdsnprmd  16323  2mulprm  16326  ge2nprmge4  16334  prmgaplem3  16682  isnzr2  20447  chrdvds  20644  chrcong  20645  lindsmm  20945  cpmidpmat  21930  csdfil  22953  iscau3  24347  ioombl1lem4  24630  itg2cn  24833  radcnvlt1  25482  sincosq1sgn  25560  sincosq3sgn  25562  sincosq4sgn  25563  ang180lem3  25866  leibpilem2  25996  issqf  26190  bposlem6  26342  gausslemma2dlem3  26421  clwlkclwwlklem2  28265  clwlkclwwlk2  28268  clwlkclwwlkf  28273  clwlknf1oclwwlknlem1  28346  konigsberglem5  28521  cvexchi  30632  addltmulALT  30709  xnn01gt  30995  dya2iocct  32147  ballotlemi1  32369  signswch  32440  usgrgt2cycl  32992  cusgracyclt3v  33018  nosupinfsep  33862  cos2h  35695  tan2h  35696  lhpocnel2  37960  cdlemk19w  38913  lcmineqlem  39988  rencldnfilem  40558  imsqrtvalex  41143  frege70  41430  frege118  41478  hashnzfzclim  41829  dvradcnv2  41854  binomcxplemnotnn0  41863  supxrleubrnmptf  42881  ioonct  42965  fourierdlem112  43649  salexct2  43768  flsqrt5  44934  lighneallem4b  44949  fpprel2  45081  gbegt5  45101  gbowgt5  45102  gbowge7  45103  gbege6  45105  sbgoldbwt  45117  sbgoldbst  45118  sbgoldbalt  45121  sbgoldbm  45124  nnsum3primesle9  45134  nnsum4primesevenALTV  45141  bgoldbtbndlem1  45145  tgblthelfgott  45155  difmodm1lt  45756