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

Theorem breq2i 4585
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
breq2i (𝐶𝑅𝐴𝐶𝑅𝐵)

Proof of Theorem breq2i
StepHypRef Expression
1 breq1i.1 . 2 𝐴 = 𝐵
2 breq2 4581 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  breqtri  4602  en1  7886  snnen2o  8011  enp1i  8057  pm54.43  8686  addclprlem2  9695  map2psrpr  9787  lt0neg2  10384  le0neg2  10386  recgt1  10768  addltmul  11115  nn0lt2  11273  3halfnz  11288  declecOLD  11376  xlt0neg2  11884  xle0neg2  11886  iccshftr  12133  iccshftl  12135  iccdil  12137  icccntr  12139  hashen1  12973  swrdccatin2  13284  swrdccat3  13289  mertens  14403  aleph1re  14759  dvdslelem  14815  3dvdsdec  14838  3dvdsdecOLD  14839  3dvds2dec  14840  3dvds2decOLD  14841  divalglem5  14904  ndvdsi  14920  bitsfzo  14941  absproddvds  15114  3prm  15190  prmfac1  15215  prm23lt5  15303  dec2dvds  15551  dec5dvds2  15553  prmlem0  15596  dprd0  18199  ablfac1lem  18236  minveclem3b  22924  minveclem6  22930  minveclem7  22931  ioombl1lem4  23053  sinhalfpilem  23936  sincosq1lem  23970  sincosq1sgn  23971  sincosq2sgn  23972  sincosq3sgn  23973  sincosq4sgn  23974  bposlem6  24731  gausslemma2dlem1a  24807  2lgsoddprmlem3  24856  avril1  26477  minvecolem5  26927  minvecolem6  26928  minvecolem7  26929  bcsiALT  27226  pjdifnormii  27732  cvexchi  28418  ballotlem4  29693  bnj110  29988  wsuclb  30827  dalem18  33781  dalem48  33820  cdlemblem  33893  cdleme7ga  34349  cdlemg27b  34798  frege116  37089  frege120  37093  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  hoidmv1lelem3  39280  hoidmvlelem3  39284  hoidmvle  39287  257prm  39809  fmtno4prmfac  39820  fmtno4nprmfac193  39822  flsqrt5  39845  139prmALT  39847  31prm  39848  127prm  39851  lighneallem2  39859  stgoldbwt  39996  nnsum3primesle9  40008  wtgoldbnnsum4prm  40016  bgoldbnnsum3prm  40018  pfxccat3  40087  lfgrwlkprop  40891  konigsberglem4  41420  lincdifsn  42002  lindslinindsimp1  42035  lindslinindsimp2lem5  42040  lindslinindsimp2  42041  fldivexpfllog2  42152  nnlog2ge0lt1  42153  blen1b  42175
  Copyright terms: Public domain W3C validator