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

Theorem subcl 9900
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 9892 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC  ( B  +  x )  =  A ) )
2 negeu 9891 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 459 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6291 . . 3  |-  ( E! x  e.  CC  ( B  +  x )  =  A  ->  ( iota_ x  e.  CC  ( B  +  x )  =  A )  e.  CC )
53, 4syl 17 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( iota_ x  e.  CC  ( B  +  x
)  =  A )  e.  CC )
61, 5eqeltrd 2540 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   E!wreu 2751   iota_crio 6276  (class class class)co 6315   CCcc 9563    + caddc 9568    - cmin 9886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706  df-sub 9888
This theorem is referenced by:  negcl  9901  subf  9903  pncan3  9909  npcan  9910  addsubass  9911  addsub  9912  addsub12  9914  addsubeq4  9916  npncan  9921  nppcan  9922  nnpcan  9923  nppcan3  9924  subcan2  9925  subsub2  9928  subsub4  9933  nnncan  9935  nnncan1  9936  nnncan2  9937  npncan3  9938  addsub4  9943  subadd4  9944  peano2cnm  9966  subcli  9976  subcld  10012  subeqrev  10070  subdi  10080  subdir  10081  mulsub2  10090  recextlem1  10270  recex  10272  mulcan1g  10293  div2sub  10460  cju  10633  halfaddsubcl  10874  halfaddsub  10875  iccf1o  11805  sersub  12288  sqsubswap  12368  subsq  12414  subsq2  12415  bcn2  12536  swrdccatin12lem2b  12879  swrdccatin12lem2  12882  shftval2  13187  2shfti  13192  sqabssub  13395  abssub  13438  abs3dif  13443  abs2dif  13444  abs2difabs  13446  climuni  13665  cjcn2  13712  recn2  13713  imcn2  13714  o1sub  13728  climsub  13746  caucvgr  13790  iseralt  13800  fsum0diag2  13893  arisum2  13968  geoserg  13973  geolim  13975  geolim2  13976  georeclim  13977  geo2sum  13978  geoisum1c  13985  fallfacval2  14113  fallfacval3  14114  fallfaccl  14118  risefallfac  14126  fallfacp1  14132  0fallfac  14139  binomfallfaclem2  14142  bpoly2  14159  bpoly3  14160  fsumcube  14162  tanadd  14270  addsin  14273  fzocongeq  14408  odd2np1  14414  divalglem9  14430  divalglem9OLD  14431  phiprm  14774  pythagtriplem4  14818  pythagtriplem12  14825  pythagtriplem14  14827  pythagtriplem16  14829  fldivp1  14891  4sqlem19  14962  vdwapun  14973  vdwlem6  14985  xrsdsreclb  19064  cnmet  21841  icccvx  22027  reparphti  22077  pcorevlem  22106  cncmet  22339  dveflem  22980  dvef  22981  dv11cn  23002  coeeulem  23227  geolim3  23344  abelthlem2  23436  abelthlem7  23442  efimpi  23495  ptolemy  23500  tangtx  23509  abssinper  23522  cosne0  23528  tanregt0  23537  eflogeq  23600  logneg2  23613  advlogexp  23649  logtayl  23654  logtayl2  23656  ang180lem1  23787  ang180lem2  23788  ang180lem3  23789  lawcos  23794  pythag  23795  isosctrlem1  23796  isosctrlem2  23797  asinlem  23843  asinlem2  23844  asinlem3a  23845  asinlem3  23846  asinf  23847  acosf  23849  atanf  23855  asinneg  23861  efiasin  23863  sinasin  23864  asinsin  23867  acoscos  23868  asinbnd  23874  cosasin  23879  atanneg  23882  atancj  23885  efiatan  23887  atanlogaddlem  23888  atanlogadd  23889  atanlogsublem  23890  atanlogsub  23891  efiatan2  23892  2efiatan  23893  cosatan  23896  atantan  23898  atanbndlem  23900  atans2  23906  dvatan  23910  atantayl  23912  atantayl2  23913  birthdaylem2  23927  scvxcvx  23960  basellem8  24063  1sgm2ppw  24177  logfacbnd3  24200  logfacrlim  24201  perfect1  24205  dchrsum2  24245  sumdchr2  24247  bposlem9  24269  lgsquad2  24337  rplogsumlem1  24371  dchrmusum2  24381  log2sumbnd  24431  pntrsumo1  24452  brbtwn2  24984  colinearalg  24989  axcgrid  24995  axsegconlem1  24996  ax5seglem1  25007  ax5seglem2  25008  ax5seglem3  25010  ax5seglem5  25012  ax5seglem9  25016  axbtwnid  25018  axeuclidlem  25041  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  axcontlem8  25050  hvmulcan2  26775  subfacp1lem6  29957  cvxscon  30015  rescon  30018  sinccvglem  30365  sin2h  31980  tan2h  31982  itg2addnclem3  32040  ftc1anclem4  32065  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anc  32070  dvasin  32073  dvacos  32074  rmspecsqrtnq  35799  jm2.17a  35855  acongeq  35878  jm2.27c  35907  lhe4.4ex1a  36722  dvconstbi  36727  abssubrp  37523  pfxccatin12lem1  39004  pfxccatin12lem2  39005  cnambpcma  39082
  Copyright terms: Public domain W3C validator