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

Theorem breq2i 4591
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 4587 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  breqtri  4608  en1  7909  snnen2o  8034  enp1i  8080  pm54.43  8709  addclprlem2  9718  map2psrpr  9810  lt0neg2  10414  le0neg2  10416  recgt1  10798  addltmul  11145  nn0lt2  11317  3halfnz  11332  declecOLD  11420  xlt0neg2  11925  xle0neg2  11927  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  hashen1  13021  swrdccatin2  13338  swrdccat3  13343  mertens  14457  aleph1re  14813  dvdslelem  14869  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  divalglem5  14958  ndvdsi  14974  bitsfzo  14995  absproddvds  15168  3prm  15244  prmfac1  15269  prm23lt5  15357  dec2dvds  15605  dec5dvds2  15607  prmlem0  15650  dprd0  18253  ablfac1lem  18290  minveclem3b  23007  minveclem6  23013  minveclem7  23014  ioombl1lem4  23136  sinhalfpilem  24019  sincosq1lem  24053  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  bposlem6  24814  gausslemma2dlem1a  24890  2lgsoddprmlem3  24939  avril1  26711  minvecolem5  27121  minvecolem6  27122  minvecolem7  27123  bcsiALT  27420  pjdifnormii  27926  cvexchi  28612  ballotlem4  29887  bnj110  30182  wsuclb  31021  dalem18  33985  dalem48  34024  cdlemblem  34097  cdleme7ga  34553  cdlemg27b  35002  frege116  37293  frege120  37297  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  hoidmv1lelem3  39483  hoidmvlelem3  39487  hoidmvle  39490  257prm  40011  fmtno4prmfac  40022  fmtno4nprmfac193  40024  flsqrt5  40047  139prmALT  40049  31prm  40050  127prm  40053  lighneallem2  40061  stgoldbwt  40198  nnsum3primesle9  40210  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  pfxccat3  40289  lfgrwlkprop  40896  konigsberglem4  41425  lincdifsn  42007  lindslinindsimp1  42040  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  fldivexpfllog2  42157  nnlog2ge0lt1  42158  blen1b  42180
  Copyright terms: Public domain W3C validator