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

Theorem breq2i 5065
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 5061 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058
This theorem is referenced by:  breqtri  5082  en1  8564  snnen2o  8695  enp1i  8741  pm54.43  9417  addclprlem2  10427  map2psrpr  10520  lt0neg2  11135  le0neg2  11137  recgt1  11524  addltmul  11861  nn0lt2  12033  3halfnz  12049  xlt0neg2  12601  xle0neg2  12603  iccshftr  12860  iccshftl  12862  iccdil  12864  icccntr  12866  hashen1  13719  swrdccatin2  14079  pfxccat3  14084  mertens  15230  aleph1re  15586  dvdslelem  15647  3dvdsdec  15669  3dvds2dec  15670  divalglem5  15736  ndvdsi  15751  bitsfzo  15772  absproddvds  15949  prmfac1  16051  prm23lt5  16139  dec2dvds  16387  dec5dvds2  16389  prmlem0  16427  dprd0  19082  ablfac1lem  19119  minveclem3b  23958  minveclem6  23964  minveclem7  23965  ioombl1lem4  24089  sinhalfpilem  24976  sincosq1lem  25010  sincosq1sgn  25011  sincosq2sgn  25012  sincosq3sgn  25013  sincosq4sgn  25014  bposlem6  25792  gausslemma2dlem1a  25868  2lgsoddprmlem3  25917  lfgrwlkprop  27396  konigsberglem4  27961  frgrwopreglem2  28019  avril1  28169  minvecolem5  28585  minvecolem6  28586  minvecolem7  28587  bcsiALT  28883  pjdifnormii  29387  cvexchi  30073  ballotlem4  31655  bnj110  32029  wsuclb  33012  dalem18  36697  dalem48  36736  cdlemblem  36809  cdleme7ga  37264  cdlemg27b  37712  frege116  40203  frege120  40207  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  hoidmv1lelem3  42752  hoidmvlelem3  42756  hoidmvle  42759  257prm  43600  fmtno4prmfac  43611  fmtno4nprmfac193  43613  flsqrt5  43634  139prmALT  43636  31prm  43637  127prm  43640  lighneallem2  43648  stgoldbwt  43818  nnsum3primesle9  43836  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  lincdifsn  44407  lindslinindsimp1  44440  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  fldivexpfllog2  44553  nnlog2ge0lt1  44554  blen1b  44576  resum2sqorgt0  44624
  Copyright terms: Public domain W3C validator