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

Theorem breq2i 5077
 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 5073 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   = wceq 1536   class class class wbr 5069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070 This theorem is referenced by:  breqtri  5094  en1  8579  snnen2o  8710  enp1i  8756  pm54.43  9432  addclprlem2  10442  map2psrpr  10535  lt0neg2  11150  le0neg2  11152  recgt1  11539  addltmul  11876  nn0lt2  12048  3halfnz  12064  xlt0neg2  12616  xle0neg2  12618  iccshftr  12875  iccshftl  12877  iccdil  12879  icccntr  12881  hashen1  13734  swrdccatin2  14094  pfxccat3  14099  mertens  15245  aleph1re  15601  dvdslelem  15662  3dvdsdec  15684  3dvds2dec  15685  divalglem5  15751  ndvdsi  15766  bitsfzo  15787  absproddvds  15964  prmfac1  16066  prm23lt5  16154  dec2dvds  16402  dec5dvds2  16404  prmlem0  16442  dprd0  19156  ablfac1lem  19193  minveclem3b  24034  minveclem6  24040  minveclem7  24041  ioombl1lem4  24165  sinhalfpilem  25052  sincosq1lem  25086  sincosq1sgn  25087  sincosq2sgn  25088  sincosq3sgn  25089  sincosq4sgn  25090  bposlem6  25868  gausslemma2dlem1a  25944  2lgsoddprmlem3  25993  lfgrwlkprop  27472  konigsberglem4  28037  frgrwopreglem2  28095  avril1  28245  minvecolem5  28661  minvecolem6  28662  minvecolem7  28663  bcsiALT  28959  pjdifnormii  29463  cvexchi  30149  ballotlem4  31760  bnj110  32134  wsuclb  33119  dalem18  36821  dalem48  36860  cdlemblem  36933  cdleme7ga  37388  cdlemg27b  37836  frege116  40331  frege120  40335  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  hoidmv1lelem3  42882  hoidmvlelem3  42886  hoidmvle  42889  257prm  43730  fmtno4prmfac  43741  fmtno4nprmfac193  43743  flsqrt5  43764  139prmALT  43766  31prm  43767  127prm  43770  lighneallem2  43778  stgoldbwt  43948  nnsum3primesle9  43966  wtgoldbnnsum4prm  43974  bgoldbnnsum3prm  43976  lincdifsn  44486  lindslinindsimp1  44519  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  fldivexpfllog2  44632  nnlog2ge0lt1  44633  blen1b  44655  resum2sqorgt0  44703
 Copyright terms: Public domain W3C validator