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

Theorem breq1i 4816
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 4812 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2ax-mp 5 1 (𝐴𝑅𝐶𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652   class class class wbr 4809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810
This theorem is referenced by:  eqbrtri  4830  brtpos0  7562  brtpos  7564  euen1  8230  euen1b  8231  2dom  8233  0sdom1dom  8365  modom2  8369  1sdom  8370  infglb  8603  infglbb  8604  cnfcom3lem  8815  pr2nelem  9078  axdclem2  9595  rnct  9600  cfpwsdom  9659  inar1  9850  reclem3pr  10124  gt0srpr  10152  mappsrpr  10182  ltpsrpr  10183  map2psrpr  10184  axpre-mulgt0  10242  lt0neg1  10788  le0neg1  10790  reclt1  11172  addltmul  11514  eluz2b1  11960  xlt0neg1  12252  xle0neg1  12254  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  elfznelfzo  12781  bernneq  13197  nn0opthlem1  13259  faclbnd4lem1  13284  hashge0  13378  hashge2el2difr  13464  cbvsum  14712  divcnvshft  14873  cbvprod  14930  iprodmul  15018  oddge22np1  15357  nn0o1gt2  15381  divalglem1  15401  divalglem6  15405  isprm3  15678  dvdsnprmd  15685  prmgaplem3  16038  isnzr2  19537  chrdvds  20149  chrcong  20150  lindsmm  20443  cpmidpmat  20957  csdfil  21977  iscau3  23355  ioombl1lem4  23619  itg2cn  23821  radcnvlt1  24463  sincosq1sgn  24542  sincosq3sgn  24544  sincosq4sgn  24545  ang180lem3  24832  leibpilem2  24959  issqf  25153  bposlem6  25305  gausslemma2dlem3  25384  clwlkclwwlklem2  27206  clwlkclwwlkf  27214  clwlknf1oclwwlknlem1  27308  konigsberglem5  27492  cvexchi  29619  addltmulALT  29696  dya2iocct  30724  ballotlemi1  30947  signswch  31021  cos2h  33756  tan2h  33757  lhpocnel2  35907  cdlemk19w  36860  rencldnfilem  37994  frege70  38833  frege118  38881  hashnzfzclim  39127  dvradcnv2  39152  binomcxplemnotnn0  39161  supxrleubrnmptf  40249  ioonct  40334  fourierdlem112  41004  salexct2  41126  flsqrt5  42117  lighneallem4b  42134  gbegt5  42257  gbowgt5  42258  gbowge7  42259  gbege6  42261  sbgoldbwt  42273  sbgoldbst  42274  sbgoldbalt  42277  sbgoldbm  42280  nnsum3primesle9  42290  nnsum4primesevenALTV  42297  bgoldbtbndlem1  42301  tgblthelfgott  42311  difmodm1lt  42918
  Copyright terms: Public domain W3C validator