MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq1i Structured version   Visualization version   GIF version

Theorem breq1i 4585
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
StepHypRef Expression
1 breq1i.1 . 2 𝐴 = 𝐵
2 breq1 4581 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2ax-mp 5 1 (𝐴𝑅𝐶𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475   class class class wbr 4578
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 4579
This theorem is referenced by:  eqbrtri  4599  brtpos0  7224  brtpos  7226  euen1  7890  euen1b  7891  2dom  7893  0sdom1dom  8021  modom2  8025  1sdom  8026  infglb  8257  infglbb  8258  cnfcom3lem  8461  pr2nelem  8688  axdclem2  9203  cfpwsdom  9263  inar1  9454  reclem3pr  9728  gt0srpr  9756  mappsrpr  9786  ltpsrpr  9787  map2psrpr  9788  axpre-mulgt0  9846  lt0neg1  10386  le0neg1  10388  reclt1  10770  addltmul  11118  eluz2b1  11594  xlt0neg1  11886  xle0neg1  11888  iccshftr  12136  iccshftl  12138  iccdil  12140  icccntr  12142  elfznelfzo  12397  bernneq  12810  nn0opthlem1  12875  faclbnd4lem1  12900  hashge0  12992  hashle00  13004  hashge2el2difr  13071  cbvsum  14222  divcnvshft  14375  cbvprod  14433  iprodmul  14522  oddge22np1  14860  nn0o1gt2  14884  divalglem1  14904  divalglem6  14908  isprm2lem  15181  isprm3  15183  dvdsnprmd  15190  prmgaplem3  15544  isnzr2  19033  chrdvds  19643  chrcong  19644  lindsmm  19934  cpmidpmat  20445  csdfil  21456  iscau3  22829  ioombl1lem4  23081  itg2cn  23281  radcnvlt1  23921  sincosq1sgn  23999  sincosq3sgn  24001  sincosq4sgn  24002  ang180lem3  24286  leibpilem2  24413  issqf  24607  bposlem6  24759  gausslemma2dlem3  24838  clwlkisclwwlklem1  26109  frgra3v  26323  3vfriswmgra  26326  numclwwlkovf2ex  26407  cvexchi  28406  addltmulALT  28483  rnct  28673  dya2iocct  29463  ballotlemi1  29685  signswch  29758  cos2h  32364  tan2h  32365  lhpocnel2  34117  cdlemk19w  35072  rencldnfilem  36196  frege70  37041  frege118  37089  hashnzfzclim  37337  dvradcnv2  37362  binomcxplemnotnn0  37371  ioonct  38405  fourierdlem112  38905  salexct2  39027  flsqrt5  39842  lighneallem4b  39859  gbegt5  39978  gbogt5  39979  gboge7  39980  gbege6  39982  bgoldbwt  39994  bgoldbst  39995  sgoldbalt  39998  nnsum3primesle9  40005  nnsum4primesevenALTV  40012  bgoldbtbndlem1  40016  tgblthelfgott  40024  tgblthelfgottOLD  40031  clwlkclwwlklem2  41201  konigsberglem5  41418  av-numclwwlkovf2ex  41509  difmodm1lt  42103
  Copyright terms: Public domain W3C validator