MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subcl Unicode version

Theorem subcl 9269
Description: Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
Assertion
Ref Expression
subcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )

Proof of Theorem subcl
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 subval 9261 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC ( B  +  x )  =  A ) )
2 negeu 9260 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 440 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6531 . . 3  |-  ( E! x  e.  CC  ( B  +  x )  =  A  ->  ( iota_ x  e.  CC ( B  +  x )  =  A )  e.  CC )
53, 4syl 16 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( iota_ x  e.  CC ( B  +  x
)  =  A )  e.  CC )
61, 5eqeltrd 2486 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   E!wreu 2676  (class class class)co 6048   iota_crio 6509   CCcc 8952    + caddc 8957    - cmin 9255
This theorem is referenced by:  negcl  9270  subf  9271  pncan3  9277  npcan  9278  addsubass  9279  addsub  9280  addsub12  9282  addsubeq4  9284  npncan  9287  nppcan  9288  nppcan3  9289  subcan2  9290  subsub2  9293  subsub4  9298  nnncan  9300  nnncan1  9301  nnncan2  9302  npncan3  9303  addsub4  9308  subadd4  9309  subcli  9340  subcld  9375  subdi  9431  subdir  9432  mulsub2  9441  recextlem1  9616  recex  9618  div2sub  9803  cju  9960  halfaddsubcl  10164  halfaddsub  10165  elnnnn0  10227  uzindOLD  10328  iccf1o  11003  sersub  11329  sqsubswap  11406  subsq  11451  subsq2  11452  bcn2  11573  shftval2  11853  2shfti  11858  sqabssub  12051  abssub  12093  abs3dif  12098  abs2dif  12099  abs2difabs  12101  climuni  12309  cjcn2  12356  recn2  12357  imcn2  12358  o1sub  12372  climsub  12390  caucvgr  12432  iseralt  12441  fsum0diag2  12529  arisum2  12603  geoserg  12608  geolim  12610  geolim2  12611  georeclim  12612  geo2sum  12613  geoisum1c  12620  tanadd  12731  addsin  12734  fzocongeq  12866  odd2np1  12871  divalglem9  12884  phiprm  13129  pythagtriplem4  13156  pythagtriplem12  13163  pythagtriplem14  13165  pythagtriplem16  13167  fldivp1  13229  4sqlem19  13294  vdwapun  13305  vdwlem6  13317  xrsdsreclb  16708  cnmet  18767  icccvx  18936  reparphti  18983  pcorevlem  19012  cncmet  19236  dveflem  19824  dvef  19825  dv11cn  19846  coeeulem  20104  geolim3  20217  abelthlem2  20309  abelthlem7  20315  efimpi  20360  ptolemy  20365  tangtx  20374  abssinper  20387  cosne0  20393  tanregt0  20402  eflogeq  20457  logneg2  20471  advlogexp  20507  logtayl  20512  logtayl2  20514  ang180lem1  20612  ang180lem2  20613  ang180lem3  20614  lawcos  20619  pythag  20620  isosctrlem1  20623  isosctrlem2  20624  asinlem  20669  asinlem2  20670  asinlem3a  20671  asinlem3  20672  asinf  20673  acosf  20675  atanf  20681  asinneg  20687  efiasin  20689  sinasin  20690  asinsin  20693  acoscos  20694  asinbnd  20700  cosasin  20705  atanneg  20708  atancj  20711  efiatan  20713  atanlogaddlem  20714  atanlogadd  20715  atanlogsublem  20716  atanlogsub  20717  efiatan2  20718  2efiatan  20719  cosatan  20722  atantan  20724  atanbndlem  20726  atans2  20732  dvatan  20736  atantayl  20738  atantayl2  20739  birthdaylem2  20752  scvxcvx  20785  basellem8  20831  1sgm2ppw  20945  logfacbnd3  20968  logfacrlim  20969  perfect1  20973  dchrsum2  21013  sumdchr2  21015  bposlem9  21037  lgsquad2  21105  rplogsumlem1  21139  dchrmusum2  21149  log2sumbnd  21199  pntrsumo1  21220  hvmulcan2  22536  subfacp1lem6  24832  cvxscon  24891  rescon  24894  sinccvglem  25070  mulcan1g  25150  subeqrev  25158  fallfacval2  25288  fallfaccl  25292  risefallfac  25300  fallfacp1  25306  0fallfac  25312  binomfallfaclem2  25315  brbtwn2  25756  colinearalg  25761  axcgrid  25767  axsegconlem1  25768  ax5seglem1  25779  ax5seglem2  25780  ax5seglem3  25782  ax5seglem5  25784  ax5seglem9  25788  axbtwnid  25790  axeuclidlem  25813  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  axcontlem8  25822  bpoly2  26015  bpoly3  26016  fsumcube  26018  itg2addnclem3  26165  rmspecsqrnq  26867  jm2.17a  26923  acongeq  26946  jm2.27c  26976  lhe4.4ex1a  27422  dvconstbi  27427  cnm1cn  27976  swrdccatin12lem3b  28030  swrdccatin12lem3  28032
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-po 4471  df-so 4472  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-riota 6516  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-ltxr 9089  df-sub 9257
  Copyright terms: Public domain W3C validator