Theorem subcl 10159

Description: Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)

Assertion

Ref	Expression
subcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Proof of Theorem subcl

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		subval 10151	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 10150	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 468	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 6525	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2688	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃!wreu 2898  ℩crio 6510  (class class class)co 6549  ℂcc 9813   + caddc 9818   − cmin 10145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-sub 10147

This theorem is referenced by:  negcl  10160  subf  10162  pncan3  10168  npcan  10169  addsubass  10170  addsub  10171  addsub12  10173  addsubeq4  10175  npncan  10181  nppcan  10182  nnpcan  10183  nppcan3  10184  subcan2  10185  subsub2  10188  subsub4  10193  nnncan  10195  nnncan1  10196  nnncan2  10197  npncan3  10198  addsub4  10203  subadd4  10204  peano2cnm  10226  subcli  10236  subcld  10271  subeqrev  10332  subdi  10342  subdir  10343  mulsub2  10353  recextlem1  10536  recex  10538  mulcan1g  10559  div2sub  10729  cju  10893  halfaddsubcl  11141  halfaddsub  11142  iccf1o  12187  modsumfzodifsn  12605  sersub  12706  sqsubswap  12786  subsq  12834  subsq2  12835  bcn2  12968  swrdccatin12lem2b  13337  swrdccatin12lem2  13340  shftval2  13663  2shfti  13668  sqabssub  13871  abssub  13914  abs3dif  13919  abs2dif  13920  abs2difabs  13922  climuni  14131  cjcn2  14178  recn2  14179  imcn2  14180  o1sub  14194  climsub  14212  caucvgr  14254  iseralt  14263  fsum0diag2  14357  arisum2  14432  geoserg  14437  geolim  14440  geolim2  14441  georeclim  14442  geo2sum  14443  geoisum1c  14450  fallfacval2  14581  fallfacval3  14582  fallfaccl  14586  risefallfac  14594  fallfacp1  14600  0fallfac  14607  binomfallfaclem2  14610  bpoly2  14627  bpoly3  14628  fsumcube  14630  tanadd  14736  addsin  14739  fzocongeq  14884  odd2np1  14903  divalglem9  14962  phiprm  15320  pythagtriplem4  15362  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  fldivp1  15439  4sqlem19  15505  vdwapun  15516  vdwlem6  15528  xrsdsreclb  19612  cnmet  22385  icccvx  22557  reparphti  22605  pcorevlem  22634  cncmet  22927  dveflem  23546  dvef  23547  dv11cn  23568  coeeulem  23784  geolim3  23898  abelthlem2  23990  abelthlem7  23996  efimpi  24047  ptolemy  24052  tangtx  24061  abssinper  24074  cosne0  24080  tanregt0  24089  eflogeq  24152  logneg2  24165  advlogexp  24201  logtayl  24206  logtayl2  24208  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  lawcos  24346  pythag  24347  isosctrlem1  24348  isosctrlem2  24349  asinlem  24395  asinlem2  24396  asinlem3a  24397  asinlem3  24398  asinf  24399  acosf  24401  atanf  24407  asinneg  24413  efiasin  24415  sinasin  24416  asinsin  24419  acoscos  24420  asinbnd  24426  cosasin  24431  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  cosatan  24448  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  birthdaylem2  24479  scvxcvx  24512  basellem8  24614  1sgm2ppw  24725  logfacbnd3  24748  logfacrlim  24749  perfect1  24753  dchrsum2  24793  sumdchr2  24795  bposlem9  24817  lgsquad2  24911  rplogsumlem1  24973  dchrmusum2  24983  log2sumbnd  25033  pntrsumo1  25054  brbtwn2  25585  colinearalg  25590  axcgrid  25596  axsegconlem1  25597  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem9  25617  axbtwnid  25619  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  hvmulcan2  27314  subfacp1lem6  30421  cvxscon  30479  rescon  30482  sinccvglem  30820  sin2h  32569  tan2h  32571  itg2addnclem3  32633  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663  dvasin  32666  dvacos  32667  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  jm2.17a  36545  acongeq  36568  jm2.27c  36592  lhe4.4ex1a  37550  dvconstbi  37555  abssubrp  38428  pfxccatin12lem1  40286  pfxccatin12lem2  40287  cnambpcma  40341  crctcsh1wlkn0lem6  41018  eucrctshift  41411