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

Theorem breq2i 4792
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 4788 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1630   class class class wbr 4784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785
This theorem is referenced by:  breqtri  4809  en1  8175  snnen2o  8304  enp1i  8350  pm54.43  9025  addclprlem2  10040  map2psrpr  10132  lt0neg2  10736  le0neg2  10738  recgt1  11120  addltmul  11469  nn0lt2  11641  3halfnz  11657  declecOLD  11745  xlt0neg2  12255  xle0neg2  12257  iccshftr  12512  iccshftl  12514  iccdil  12516  icccntr  12518  hashen1  13361  swrdccatin2  13695  swrdccat3  13700  mertens  14824  aleph1re  15179  dvdslelem  15239  3dvdsdec  15262  3dvdsdecOLD  15263  3dvds2dec  15264  divalglem5  15327  ndvdsi  15343  bitsfzo  15364  absproddvds  15537  3prm  15612  prmfac1  15637  prm23lt5  15725  dec2dvds  15973  dec5dvds2  15975  prmlem0  16018  dprd0  18637  ablfac1lem  18674  minveclem3b  23417  minveclem6  23423  minveclem7  23424  ioombl1lem4  23548  sinhalfpilem  24435  sincosq1lem  24469  sincosq1sgn  24470  sincosq2sgn  24471  sincosq3sgn  24472  sincosq4sgn  24473  bposlem6  25234  gausslemma2dlem1a  25310  2lgsoddprmlem3  25359  lfgrwlkprop  26818  konigsberglem4  27432  frgrwopreglem2  27492  avril1  27655  minvecolem5  28071  minvecolem6  28072  minvecolem7  28073  bcsiALT  28370  pjdifnormii  28876  cvexchi  29562  ballotlem4  30894  bnj110  31260  wsuclb  32104  dalem18  35482  dalem48  35521  cdlemblem  35594  cdleme7ga  36050  cdlemg27b  36498  frege116  38792  frege120  38796  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  hoidmv1lelem3  41321  hoidmvlelem3  41325  hoidmvle  41328  pfxccat3  41944  257prm  41991  fmtno4prmfac  42002  fmtno4nprmfac193  42004  flsqrt5  42027  139prmALT  42029  31prm  42030  127prm  42033  lighneallem2  42041  stgoldbwt  42182  nnsum3primesle9  42200  wtgoldbnnsum4prm  42208  bgoldbnnsum3prm  42210  lincdifsn  42731  lindslinindsimp1  42764  lindslinindsimp2lem5  42769  lindslinindsimp2  42770  fldivexpfllog2  42877  nnlog2ge0lt1  42878  blen1b  42900
  Copyright terms: Public domain W3C validator