Theorem breq1i 5082

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  eqbrtri  5096  brtpos0  8058  brtpos  8060  euen1  8825  euen1b  8826  2dom  8829  0sdom1dom  9029  modom2  9033  1sdom  9034  infglb  9258  infglbb  9259  cnfcom3lem  9470  pr2nelem  9769  axdclem2  10285  rnct  10290  cfpwsdom  10349  inar1  10540  reclem3pr  10814  gt0srpr  10843  mappsrpr  10873  ltpsrpr  10874  map2psrpr  10875  axpre-mulgt0  10933  lt0neg1  11490  le0neg1  11492  reclt1  11879  addltmul  12218  eluz2b1  12668  xlt0neg1  12962  xle0neg1  12964  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  elfznelfzo  13501  bernneq  13953  nn0opthlem1  13991  faclbnd4lem1  14016  hashge0  14111  hashgt23el  14148  hashge2el2difr  14204  cbvsum  15416  divcnvshft  15576  cbvprod  15634  iprodmul  15722  oddge22np1  16067  nn0o1gt2  16099  divalglem1  16112  divalglem6  16116  isprm3  16397  dvdsnprmd  16404  2mulprm  16407  ge2nprmge4  16415  prmgaplem3  16763  isnzr2  20543  chrdvds  20741  chrcong  20742  lindsmm  21044  cpmidpmat  22031  csdfil  23054  iscau3  24451  ioombl1lem4  24734  itg2cn  24937  radcnvlt1  25586  sincosq1sgn  25664  sincosq3sgn  25666  sincosq4sgn  25667  ang180lem3  25970  leibpilem2  26100  issqf  26294  bposlem6  26446  gausslemma2dlem3  26525  clwlkclwwlklem2  28373  clwlkclwwlk2  28376  clwlkclwwlkf  28381  clwlknf1oclwwlknlem1  28454  konigsberglem5  28629  cvexchi  30740  addltmulALT  30817  xnn01gt  31102  dya2iocct  32256  ballotlemi1  32478  signswch  32549  usgrgt2cycl  33101  cusgracyclt3v  33127  nosupinfsep  33944  cos2h  35777  tan2h  35778  lhpocnel2  38040  cdlemk19w  38993  lcmineqlem  40067  rencldnfilem  40649  imsqrtvalex  41261  frege70  41548  frege118  41596  hashnzfzclim  41947  dvradcnv2  41972  binomcxplemnotnn0  41981  supxrleubrnmptf  42998  ioonct  43082  fourierdlem112  43766  salexct2  43885  flsqrt5  45057  lighneallem4b  45072  fpprel2  45204  gbegt5  45224  gbowgt5  45225  gbowge7  45226  gbege6  45228  sbgoldbwt  45240  sbgoldbst  45241  sbgoldbalt  45244  sbgoldbm  45247  nnsum3primesle9  45257  nnsum4primesevenALTV  45264  bgoldbtbndlem1  45268  tgblthelfgott  45278  difmodm1lt  45879