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

Theorem breq1i 4692
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
breq1i (𝐴𝑅𝐶𝐵𝑅𝐶)

Proof of Theorem breq1i
StepHypRef Expression
1 breq1i.1 . 2 𝐴 = 𝐵
2 breq1 4688 . 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:  eqbrtri  4706  brtpos0  7404  brtpos  7406  euen1  8067  euen1b  8068  2dom  8070  0sdom1dom  8199  modom2  8203  1sdom  8204  infglb  8437  infglbb  8438  cnfcom3lem  8638  pr2nelem  8865  axdclem2  9380  rnct  9385  cfpwsdom  9444  inar1  9635  reclem3pr  9909  gt0srpr  9937  mappsrpr  9967  ltpsrpr  9968  map2psrpr  9969  axpre-mulgt0  10027  lt0neg1  10572  le0neg1  10574  reclt1  10956  addltmul  11306  eluz2b1  11797  xlt0neg1  12088  xle0neg1  12090  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  elfznelfzo  12613  bernneq  13030  nn0opthlem1  13095  faclbnd4lem1  13120  hashge0  13214  hashge2el2difr  13301  cbvsum  14469  divcnvshft  14631  cbvprod  14689  iprodmul  14778  oddge22np1  15120  nn0o1gt2  15144  divalglem1  15164  divalglem6  15168  isprm3  15443  dvdsnprmd  15450  prmgaplem3  15804  isnzr2  19311  chrdvds  19924  chrcong  19925  lindsmm  20215  cpmidpmat  20726  csdfil  21745  iscau3  23122  ioombl1lem4  23375  itg2cn  23575  radcnvlt1  24217  sincosq1sgn  24295  sincosq3sgn  24297  sincosq4sgn  24298  ang180lem3  24586  leibpilem2  24713  issqf  24907  bposlem6  25059  gausslemma2dlem3  25138  clwlkclwwlklem2  26966  konigsberglem5  27234  cvexchi  29356  addltmulALT  29433  dya2iocct  30470  ballotlemi1  30692  signswch  30766  cos2h  33530  tan2h  33531  lhpocnel2  35623  cdlemk19w  36577  rencldnfilem  37701  frege70  38544  frege118  38592  hashnzfzclim  38838  dvradcnv2  38863  binomcxplemnotnn0  38872  supxrleubrnmptf  39993  ioonct  40082  fourierdlem112  40753  salexct2  40875  flsqrt5  41834  lighneallem4b  41851  gbegt5  41974  gbowgt5  41975  gbowge7  41976  gbege6  41978  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbalt  41994  sbgoldbm  41997  nnsum3primesle9  42007  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  tgblthelfgott  42028  tgblthelfgottOLD  42034  difmodm1lt  42642
  Copyright terms: Public domain W3C validator