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

Theorem breq2i 4659
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 4655 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1482   class class class wbr 4651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-br 4652
This theorem is referenced by:  breqtri  4676  en1  8020  snnen2o  8146  enp1i  8192  pm54.43  8823  addclprlem2  9836  map2psrpr  9928  lt0neg2  10532  le0neg2  10534  recgt1  10916  addltmul  11265  nn0lt2  11437  3halfnz  11453  declecOLD  11541  xlt0neg2  12048  xle0neg2  12050  iccshftr  12303  iccshftl  12305  iccdil  12307  icccntr  12309  hashen1  13155  swrdccatin2  13481  swrdccat3  13486  mertens  14612  aleph1re  14968  dvdslelem  15025  3dvdsdec  15048  3dvdsdecOLD  15049  3dvds2dec  15050  3dvds2decOLD  15051  divalglem5  15114  ndvdsi  15130  bitsfzo  15151  absproddvds  15324  3prm  15400  prmfac1  15425  prm23lt5  15513  dec2dvds  15761  dec5dvds2  15763  prmlem0  15806  dprd0  18424  ablfac1lem  18461  minveclem3b  23193  minveclem6  23199  minveclem7  23200  ioombl1lem4  23323  sinhalfpilem  24209  sincosq1lem  24243  sincosq1sgn  24244  sincosq2sgn  24245  sincosq3sgn  24246  sincosq4sgn  24247  bposlem6  25008  gausslemma2dlem1a  25084  2lgsoddprmlem3  25133  lfgrwlkprop  26578  konigsberglem4  27110  frgrwopreglem2  27168  avril1  27303  minvecolem5  27721  minvecolem6  27722  minvecolem7  27723  bcsiALT  28020  pjdifnormii  28526  cvexchi  29212  ballotlem4  30545  bnj110  30913  wsuclb  31761  dalem18  34793  dalem48  34832  cdlemblem  34905  cdleme7ga  35361  cdlemg27b  35810  frege116  38099  frege120  38103  ioodvbdlimc1lem2  39916  ioodvbdlimc2lem  39918  hoidmv1lelem3  40576  hoidmvlelem3  40580  hoidmvle  40583  pfxccat3  41197  257prm  41244  fmtno4prmfac  41255  fmtno4nprmfac193  41257  flsqrt5  41280  139prmALT  41282  31prm  41283  127prm  41286  lighneallem2  41294  stgoldbwt  41435  nnsum3primesle9  41453  wtgoldbnnsum4prm  41461  bgoldbnnsum3prm  41463  lincdifsn  41984  lindslinindsimp1  42017  lindslinindsimp2lem5  42022  lindslinindsimp2  42023  fldivexpfllog2  42130  nnlog2ge0lt1  42131  blen1b  42153
  Copyright terms: Public domain W3C validator