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

Theorem breq2i 4693
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 4689 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2ax-mp 5 1 (𝐶𝑅𝐴𝐶𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  breqtri  4710  en1  8064  snnen2o  8190  enp1i  8236  pm54.43  8864  addclprlem2  9877  map2psrpr  9969  lt0neg2  10573  le0neg2  10575  recgt1  10957  addltmul  11306  nn0lt2  11478  3halfnz  11494  declecOLD  11582  xlt0neg2  12089  xle0neg2  12091  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  hashen1  13198  swrdccatin2  13533  swrdccat3  13538  mertens  14662  aleph1re  15018  dvdslelem  15078  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  divalglem5  15167  ndvdsi  15183  bitsfzo  15204  absproddvds  15377  3prm  15453  prmfac1  15478  prm23lt5  15566  dec2dvds  15814  dec5dvds2  15816  prmlem0  15859  dprd0  18476  ablfac1lem  18513  minveclem3b  23245  minveclem6  23251  minveclem7  23252  ioombl1lem4  23375  sinhalfpilem  24260  sincosq1lem  24294  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  bposlem6  25059  gausslemma2dlem1a  25135  2lgsoddprmlem3  25184  lfgrwlkprop  26640  konigsberglem4  27233  frgrwopreglem2  27293  avril1  27449  minvecolem5  27865  minvecolem6  27866  minvecolem7  27867  bcsiALT  28164  pjdifnormii  28670  cvexchi  29356  ballotlem4  30688  bnj110  31054  wsuclb  31898  dalem18  35285  dalem48  35324  cdlemblem  35397  cdleme7ga  35853  cdlemg27b  36301  frege116  38590  frege120  38594  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  hoidmv1lelem3  41128  hoidmvlelem3  41132  hoidmvle  41135  pfxccat3  41751  257prm  41798  fmtno4prmfac  41809  fmtno4nprmfac193  41811  flsqrt5  41834  139prmALT  41836  31prm  41837  127prm  41840  lighneallem2  41848  stgoldbwt  41989  nnsum3primesle9  42007  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  lincdifsn  42538  lindslinindsimp1  42571  lindslinindsimp2lem5  42576  lindslinindsimp2  42577  fldivexpfllog2  42684  nnlog2ge0lt1  42685  blen1b  42707
  Copyright terms: Public domain W3C validator