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  43883  ioodvbdlimc2lem  43885  hoidmv1lelem3  44542  hoidmvlelem3  44546  hoidmvle  44549  257prm  45453  fmtno4prmfac  45464  fmtno4nprmfac193  45466  flsqrt5  45486  139prmALT  45488  31prm  45489  127prm  45491  lighneallem2  45498  stgoldbwt  45668  nnsum3primesle9  45686  wtgoldbnnsum4prm  45694  bgoldbnnsum3prm  45696  lincdifsn  46205  lindslinindsimp1  46238  lindslinindsimp2lem5  46243  lindslinindsimp2  46244  fldivexpfllog2  46351  nnlog2ge0lt1  46352  blen1b  46374  resum2sqorgt0  46495
  Copyright terms: Public domain W3C validator