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

Theorem subcl 9863
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 9855 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC  ( B  +  x )  =  A ) )
2 negeu 9854 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 454 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6272 . . 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 2508 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1867   E!wreu 2775   iota_crio 6257  (class class class)co 6296   CCcc 9526    + caddc 9531    - cmin 9849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-po 4766  df-so 4767  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 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-ltxr 9669  df-sub 9851
This theorem is referenced by:  negcl  9864  subf  9866  pncan3  9872  npcan  9873  addsubass  9874  addsub  9875  addsub12  9877  addsubeq4  9879  npncan  9884  nppcan  9885  nnpcan  9886  nppcan3  9887  subcan2  9888  subsub2  9891  subsub4  9896  nnncan  9898  nnncan1  9899  nnncan2  9900  npncan3  9901  addsub4  9906  subadd4  9907  peano2cnm  9929  subcli  9939  subcld  9975  subeqrev  10031  subdi  10041  subdir  10042  mulsub2  10051  recextlem1  10231  recex  10233  mulcan1g  10254  div2sub  10421  cju  10594  halfaddsubcl  10834  halfaddsub  10835  iccf1o  11763  sersub  12242  sqsubswap  12322  subsq  12368  subsq2  12369  bcn2  12490  swrdccatin12lem2b  12816  swrdccatin12lem2  12819  shftval2  13106  2shfti  13111  sqabssub  13314  abssub  13357  abs3dif  13362  abs2dif  13363  abs2difabs  13365  climuni  13583  cjcn2  13630  recn2  13631  imcn2  13632  o1sub  13646  climsub  13664  caucvgr  13708  iseralt  13718  fsum0diag2  13811  arisum2  13886  geoserg  13891  geolim  13893  geolim2  13894  georeclim  13895  geo2sum  13896  geoisum1c  13903  fallfacval2  14031  fallfacval3  14032  fallfaccl  14036  risefallfac  14044  fallfacp1  14050  0fallfac  14057  binomfallfaclem2  14060  bpoly2  14077  bpoly3  14078  fsumcube  14080  tanadd  14188  addsin  14191  fzocongeq  14326  odd2np1  14332  divalglem9  14346  phiprm  14683  pythagtriplem4  14721  pythagtriplem12  14728  pythagtriplem14  14730  pythagtriplem16  14732  fldivp1  14794  4sqlem19  14865  vdwapun  14876  vdwlem6  14888  xrsdsreclb  18943  cnmet  21696  icccvx  21867  reparphti  21914  pcorevlem  21943  cncmet  22176  dveflem  22805  dvef  22806  dv11cn  22827  coeeulem  23043  geolim3  23157  abelthlem2  23249  abelthlem7  23255  efimpi  23308  ptolemy  23313  tangtx  23322  abssinper  23335  cosne0  23341  tanregt0  23350  eflogeq  23413  logneg2  23426  advlogexp  23462  logtayl  23467  logtayl2  23469  ang180lem1  23600  ang180lem2  23601  ang180lem3  23602  lawcos  23607  pythag  23608  isosctrlem1  23609  isosctrlem2  23610  asinlem  23656  asinlem2  23657  asinlem3a  23658  asinlem3  23659  asinf  23660  acosf  23662  atanf  23668  asinneg  23674  efiasin  23676  sinasin  23677  asinsin  23680  acoscos  23681  asinbnd  23687  cosasin  23692  atanneg  23695  atancj  23698  efiatan  23700  atanlogaddlem  23701  atanlogadd  23702  atanlogsublem  23703  atanlogsub  23704  efiatan2  23705  2efiatan  23706  cosatan  23709  atantan  23711  atanbndlem  23713  atans2  23719  dvatan  23723  atantayl  23725  atantayl2  23726  birthdaylem2  23740  scvxcvx  23773  basellem8  23874  1sgm2ppw  23988  logfacbnd3  24011  logfacrlim  24012  perfect1  24016  dchrsum2  24056  sumdchr2  24058  bposlem9  24080  lgsquad2  24148  rplogsumlem1  24182  dchrmusum2  24192  log2sumbnd  24242  pntrsumo1  24263  brbtwn2  24778  colinearalg  24783  axcgrid  24789  axsegconlem1  24790  ax5seglem1  24801  ax5seglem2  24802  ax5seglem3  24804  ax5seglem5  24806  ax5seglem9  24810  axbtwnid  24812  axeuclidlem  24835  axcontlem2  24838  axcontlem4  24840  axcontlem7  24843  axcontlem8  24844  hvmulcan2  26558  subfacp1lem6  29693  cvxscon  29751  rescon  29754  sinccvglem  30101  sin2h  31639  tan2h  31641  itg2addnclem3  31699  ftc1anclem4  31724  ftc1anclem5  31725  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anc  31729  dvasin  31732  dvacos  31733  rmspecsqrtnq  35464  jm2.17a  35520  acongeq  35543  jm2.27c  35572  lhe4.4ex1a  36319  dvconstbi  36324  abssubrp  37098  pfxccatin12lem1  38367  pfxccatin12lem2  38368  cnambpcma  38402
  Copyright terms: Public domain W3C validator