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

Theorem breq2i 5111
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 5107 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541   class class class wbr 5103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104
This theorem is referenced by:  breqtri  5128  en1  8898  en1OLD  8899  snnen2oOLD  9104  sdom1  9119  enp1i  9156  enp1iOLD  9157  pm54.43  9870  addclprlem2  10886  map2psrpr  10979  lt0neg2  11595  le0neg2  11597  recgt1  11984  addltmul  12322  nn0lt2  12496  3halfnz  12512  xlt0neg2  13067  xle0neg2  13069  iccshftr  13331  iccshftl  13333  iccdil  13335  icccntr  13337  hashen1  14197  swrdccatin2  14548  pfxccat3  14553  mertens  15705  aleph1re  16061  dvdslelem  16125  3dvdsdec  16148  3dvds2dec  16149  divalglem5  16213  ndvdsi  16228  bitsfzo  16249  absproddvds  16427  prmfac1  16531  prm23lt5  16620  dec2dvds  16869  dec5dvds2  16871  prmlem0  16912  dprd0  19739  ablfac1lem  19776  minveclem3b  24714  minveclem6  24720  minveclem7  24721  ioombl1lem4  24847  sinhalfpilem  25742  sincosq1lem  25776  sincosq1sgn  25777  sincosq2sgn  25778  sincosq3sgn  25779  sincosq4sgn  25780  bposlem6  26559  gausslemma2dlem1a  26635  2lgsoddprmlem3  26684  nosupinfsep  27002  lfgrwlkprop  28433  konigsberglem4  28997  frgrwopreglem2  29055  avril1  29205  minvecolem5  29621  minvecolem6  29622  minvecolem7  29623  bcsiALT  29919  pjdifnormii  30423  cvexchi  31109  ballotlem4  32871  bnj110  33243  wsuclb  34207  dalem18  38039  dalem48  38078  cdlemblem  38151  cdleme7ga  38606  cdlemg27b  39054  frege116  42013  frege120  42017  ioodvbdlimc1lem2  43926  ioodvbdlimc2lem  43928  hoidmv1lelem3  44587  hoidmvlelem3  44591  hoidmvle  44594  257prm  45502  fmtno4prmfac  45513  fmtno4nprmfac193  45515  flsqrt5  45535  139prmALT  45537  31prm  45538  127prm  45540  lighneallem2  45547  stgoldbwt  45717  nnsum3primesle9  45735  wtgoldbnnsum4prm  45743  bgoldbnnsum3prm  45745  lincdifsn  46254  lindslinindsimp1  46287  lindslinindsimp2lem5  46292  lindslinindsimp2  46293  fldivexpfllog2  46400  nnlog2ge0lt1  46401  blen1b  46423  resum2sqorgt0  46544
  Copyright terms: Public domain W3C validator