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

Theorem breq1i 5069
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 5065 . 2 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
31, 2ax-mp 5 1 (𝐴𝑅𝐶𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1530   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063
This theorem is referenced by:  eqbrtri  5083  brtpos0  7893  brtpos  7895  euen1  8571  euen1b  8572  2dom  8574  0sdom1dom  8708  modom2  8712  1sdom  8713  infglb  8946  infglbb  8947  cnfcom3lem  9158  pr2nelem  9422  axdclem2  9934  rnct  9939  cfpwsdom  9998  inar1  10189  reclem3pr  10463  gt0srpr  10492  mappsrpr  10522  ltpsrpr  10523  map2psrpr  10524  axpre-mulgt0  10582  lt0neg1  11138  le0neg1  11140  reclt1  11527  addltmul  11865  eluz2b1  12311  xlt0neg1  12605  xle0neg1  12607  iccshftr  12865  iccshftl  12867  iccdil  12869  icccntr  12871  elfznelfzo  13135  bernneq  13583  nn0opthlem1  13621  faclbnd4lem1  13646  hashge0  13741  hashgt23el  13778  hashge2el2difr  13832  cbvsum  15045  divcnvshft  15203  cbvprod  15262  iprodmul  15350  oddge22np1  15691  nn0o1gt2  15725  divalglem1  15738  divalglem6  15742  isprm3  16020  dvdsnprmd  16027  2mulprm  16030  ge2nprmge4  16038  prmgaplem3  16382  isnzr2  19958  chrdvds  20594  chrcong  20595  lindsmm  20891  cpmidpmat  21400  csdfil  22421  iscau3  23799  ioombl1lem4  24080  itg2cn  24282  radcnvlt1  24924  sincosq1sgn  25002  sincosq3sgn  25004  sincosq4sgn  25005  ang180lem3  25305  leibpilem2  25436  issqf  25630  bposlem6  25782  gausslemma2dlem3  25861  clwlkclwwlklem2  27695  clwlkclwwlk2  27698  clwlkclwwlkf  27703  clwlknf1oclwwlknlem1  27777  konigsberglem5  27952  cvexchi  30063  addltmulALT  30140  xnn01gt  30411  dya2iocct  31427  ballotlemi1  31649  signswch  31720  usgrgt2cycl  32264  cusgracyclt3v  32290  cos2h  34753  tan2h  34754  lhpocnel2  37025  cdlemk19w  37978  rencldnfilem  39285  frege70  40147  frege118  40195  hashnzfzclim  40522  dvradcnv2  40547  binomcxplemnotnn0  40556  supxrleubrnmptf  41595  ioonct  41681  fourierdlem112  42372  salexct2  42491  flsqrt5  43592  lighneallem4b  43609  fpprel2  43741  gbegt5  43761  gbowgt5  43762  gbowge7  43763  gbege6  43765  sbgoldbwt  43777  sbgoldbst  43778  sbgoldbalt  43781  sbgoldbm  43784  nnsum3primesle9  43794  nnsum4primesevenALTV  43801  bgoldbtbndlem1  43805  tgblthelfgott  43815  difmodm1lt  44417
  Copyright terms: Public domain W3C validator