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

Theorem breq2i 5112
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 5108 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542   class class class wbr 5104
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 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105
This theorem is referenced by:  breqtri  5129  en1  8899  en1OLD  8900  snnen2oOLD  9105  sdom1  9120  enp1i  9157  enp1iOLD  9158  pm54.43  9871  addclprlem2  10887  map2psrpr  10980  lt0neg2  11596  le0neg2  11598  recgt1  11985  addltmul  12323  nn0lt2  12497  3halfnz  12513  xlt0neg2  13068  xle0neg2  13070  iccshftr  13332  iccshftl  13334  iccdil  13336  icccntr  13338  hashen1  14198  swrdccatin2  14549  pfxccat3  14554  mertens  15706  aleph1re  16062  dvdslelem  16126  3dvdsdec  16149  3dvds2dec  16150  divalglem5  16214  ndvdsi  16229  bitsfzo  16250  absproddvds  16428  prmfac1  16532  prm23lt5  16621  dec2dvds  16870  dec5dvds2  16872  prmlem0  16913  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  28421  konigsberglem4  28985  frgrwopreglem2  29043  avril1  29193  minvecolem5  29609  minvecolem6  29610  minvecolem7  29611  bcsiALT  29907  pjdifnormii  30411  cvexchi  31097  ballotlem4  32859  bnj110  33231  wsuclb  34195  dalem18  38030  dalem48  38069  cdlemblem  38142  cdleme7ga  38597  cdlemg27b  39045  frege116  41982  frege120  41986  ioodvbdlimc1lem2  43895  ioodvbdlimc2lem  43897  hoidmv1lelem3  44556  hoidmvlelem3  44560  hoidmvle  44563  257prm  45471  fmtno4prmfac  45482  fmtno4nprmfac193  45484  flsqrt5  45504  139prmALT  45506  31prm  45507  127prm  45509  lighneallem2  45516  stgoldbwt  45686  nnsum3primesle9  45704  wtgoldbnnsum4prm  45712  bgoldbnnsum3prm  45714  lincdifsn  46223  lindslinindsimp1  46256  lindslinindsimp2lem5  46261  lindslinindsimp2  46262  fldivexpfllog2  46369  nnlog2ge0lt1  46370  blen1b  46392  resum2sqorgt0  46513
  Copyright terms: Public domain W3C validator