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

Theorem subcl 9141
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 9133 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC ( B  +  x )  =  A ) )
2 negeu 9132 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 439 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6406 . . 3  |-  ( E! x  e.  CC  ( B  +  x )  =  A  ->  ( iota_ x  e.  CC ( B  +  x )  =  A )  e.  CC )
53, 4syl 15 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( iota_ x  e.  CC ( B  +  x
)  =  A )  e.  CC )
61, 5eqeltrd 2432 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   E!wreu 2621  (class class class)co 5945   iota_crio 6384   CCcc 8825    + caddc 8830    - cmin 9127
This theorem is referenced by:  negcl  9142  subf  9143  pncan3  9149  npcan  9150  addsubass  9151  addsub  9152  addsub12  9154  addsubeq4  9156  npncan  9159  nppcan  9160  nppcan3  9161  subcan2  9162  subsub2  9165  subsub4  9170  nnncan  9172  nnncan1  9173  nnncan2  9174  npncan3  9175  addsub4  9180  subadd4  9181  subcli  9212  subcld  9247  subdi  9303  subdir  9304  mulsub2  9313  recextlem1  9488  recex  9490  div2sub  9675  cju  9832  halfaddsubcl  10036  halfaddsub  10037  elnnnn0  10099  uzindOLD  10198  iccf1o  10870  sersub  11181  sqsubswap  11258  subsq  11303  subsq2  11304  bcn2  11424  shftval2  11666  2shfti  11671  sqabssub  11864  abssub  11906  abs3dif  11911  abs2dif  11912  abs2difabs  11914  climuni  12122  cjcn2  12169  recn2  12170  imcn2  12171  o1sub  12185  climsub  12203  caucvgr  12245  iseralt  12254  fsum0diag2  12342  arisum2  12416  geoserg  12421  geolim  12423  geolim2  12424  georeclim  12425  geo2sum  12426  geoisum1c  12433  tanadd  12544  addsin  12547  fzocongeq  12679  odd2np1  12684  divalglem9  12697  phiprm  12942  pythagtriplem4  12969  pythagtriplem12  12976  pythagtriplem14  12978  pythagtriplem16  12980  fldivp1  13042  4sqlem19  13107  vdwapun  13118  vdwlem6  13130  xrsdsreclb  16524  cnmet  18383  icccvx  18552  reparphti  18599  pcorevlem  18628  cncmet  18848  dveflem  19430  dvef  19431  dv11cn  19452  coeeulem  19710  geolim3  19823  abelthlem2  19915  abelthlem7  19921  efimpi  19966  ptolemy  19971  tangtx  19980  abssinper  19993  cosne0  19999  tanregt0  20008  eflogeq  20063  logneg2  20077  advlogexp  20113  logtayl  20118  logtayl2  20120  ang180lem1  20218  ang180lem2  20219  ang180lem3  20220  lawcos  20225  pythag  20226  isosctrlem1  20229  isosctrlem2  20230  asinlem  20275  asinlem2  20276  asinlem3a  20277  asinlem3  20278  asinf  20279  acosf  20281  atanf  20287  asinneg  20293  efiasin  20295  sinasin  20296  asinsin  20299  acoscos  20300  asinbnd  20306  cosasin  20311  atanneg  20314  atancj  20317  efiatan  20319  atanlogaddlem  20320  atanlogadd  20321  atanlogsublem  20322  atanlogsub  20323  efiatan2  20324  2efiatan  20325  cosatan  20328  atantan  20330  atanbndlem  20332  atans2  20338  dvatan  20342  atantayl  20344  atantayl2  20345  birthdaylem2  20358  scvxcvx  20391  basellem8  20437  1sgm2ppw  20551  logfacbnd3  20574  logfacrlim  20575  perfect1  20579  dchrsum2  20619  sumdchr2  20621  bposlem9  20643  lgsquad2  20711  rplogsumlem1  20745  dchrmusum2  20755  log2sumbnd  20805  pntrsumo1  20826  hvmulcan2  21766  subfacp1lem6  24120  cvxscon  24178  rescon  24181  sinccvglem  24409  mulcan1g  24490  subeqrev  24498  fallfacval2  24618  fallfaccl  24622  fallfacp1  24635  risefallfac  24640  brbtwn2  25092  colinearalg  25097  axcgrid  25103  axsegconlem1  25104  ax5seglem1  25115  ax5seglem2  25116  ax5seglem3  25118  ax5seglem5  25120  ax5seglem9  25124  axbtwnid  25126  axeuclidlem  25149  axcontlem2  25152  axcontlem4  25154  axcontlem7  25157  axcontlem8  25158  bpoly2  25351  bpoly3  25352  fsumcube  25354  rmspecsqrnq  26314  jm2.17a  26370  acongeq  26393  jm2.27c  26423  lhe4.4ex1a  26869  dvconstbi  26874  stoweidlem1  27073  stoweidlem11  27083  stoweidlem13  27085  stoweidlem26  27098  stoweid  27135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-po 4396  df-so 4397  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-riota 6391  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-pnf 8959  df-mnf 8960  df-ltxr 8962  df-sub 9129
  Copyright terms: Public domain W3C validator