Theorem subcl 11379

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 11371	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11370	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 458	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7332	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2836	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃!wreu 3348  ℩crio 7314  (class class class)co 7358  ℂcc 11024   + caddc 11029   − cmin 11364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366

This theorem is referenced by:  negcl  11380  subf  11382  pncan3  11388  npcan  11389  addsubass  11390  addsub  11391  addsub12  11393  addsubeq4  11395  npncan  11402  nppcan  11403  nnpcan  11404  nppcan3  11405  subcan2  11406  subsub2  11409  subsub4  11414  nnncan  11416  nnncan1  11417  nnncan2  11418  npncan3  11419  addsub4  11424  subadd4  11425  peano2cnm  11447  subcli  11457  subcld  11492  subeqrev  11559  subdi  11570  subdir  11571  mulsub2  11581  recextlem1  11767  recex  11769  mulcan1g  11790  div2sub  11966  cju  12141  halfaddsubcl  12373  halfaddsub  12374  iccf1o  13412  modsumfzodifsn  13867  sersub  13968  sqsubswap  14040  subsq  14133  subsq2  14134  bcn2  14242  pfxccatin12lem1  14651  pfxccatin12lem2  14654  shftval2  14998  2shfti  15003  sqabssub  15206  abssub  15250  abs3dif  15255  abs2dif  15256  abs2difabs  15258  climuni  15475  cjcn2  15523  recn2  15524  imcn2  15525  o1sub  15539  climsub  15557  caucvgr  15599  iseralt  15608  fsum0diag2  15706  arisum2  15784  geoserg  15789  geolim  15793  geolim2  15794  georeclim  15795  geo2sum  15796  geoisum1c  15803  fallfacval2  15934  fallfacval3  15935  fallfaccl  15939  risefallfac  15947  fallfacp1  15953  0fallfac  15960  binomfallfaclem2  15963  bpoly2  15980  bpoly3  15981  fsumcube  15983  tanadd  16092  addsin  16095  fzocongeq  16251  odd2np1  16268  divalglem9  16328  phiprm  16704  pythagtriplem4  16747  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  fldivp1  16825  4sqlem19  16891  vdwapun  16902  vdwlem6  16914  xrsdsreclb  21368  cnmet  24715  icccvx  24904  reparphti  24952  reparphtiOLD  24953  pcorevlem  24982  cncmet  25278  dveflem  25939  dvef  25940  dv11cn  25962  coeeulem  26185  geolim3  26303  abelthlem2  26398  abelthlem7  26404  efimpi  26456  ptolemy  26461  tangtx  26470  abssinper  26486  cosne0  26494  tanregt0  26504  eflogeq  26567  logneg2  26580  advlogexp  26620  logtayl  26625  logtayl2  26627  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  lawcos  26782  pythag  26783  isosctrlem1  26784  isosctrlem2  26785  asinlem  26834  asinlem2  26835  asinlem3a  26836  asinlem3  26837  asinf  26838  acosf  26840  atanf  26846  asinneg  26852  efiasin  26854  sinasin  26855  asinsin  26858  acoscos  26859  asinbnd  26865  cosasin  26870  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsublem  26881  atanlogsub  26882  efiatan2  26883  2efiatan  26884  cosatan  26887  atantan  26889  atanbndlem  26891  atans2  26897  dvatan  26901  atantayl  26903  atantayl2  26904  birthdaylem2  26918  scvxcvx  26952  basellem8  27054  1sgm2ppw  27167  logfacbnd3  27190  logfacrlim  27191  perfect1  27195  dchrsum2  27235  sumdchr2  27237  bposlem9  27259  lgsquad2  27353  addsq2reu  27407  rplogsumlem1  27451  dchrmusum2  27461  log2sumbnd  27511  pntrsumo1  27532  brbtwn2  28978  colinearalg  28983  axcgrid  28989  axsegconlem1  28990  ax5seglem1  29001  ax5seglem2  29002  ax5seglem3  29004  ax5seglem5  29006  ax5seglem9  29010  axbtwnid  29012  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  crctcshwlkn0lem6  29888  eucrctshift  30318  hvmulcan2  31148  subfacp1lem6  35379  cvxsconn  35437  resconn  35440  sinccvglem  35866  sin2h  37807  tan2h  37809  itg2addnclem3  37870  ftc1anclem4  37893  ftc1anclem5  37894  ftc1anclem6  37895  ftc1anclem7  37896  ftc1anc  37898  dvasin  37901  dvacos  37902  lcmineqlem4  42282  lcmineqlem8  42286  rmspecsqrtnq  43144  jm2.17a  43198  acongeq  43221  jm2.27c  43245  lhe4.4ex1a  44566  dvconstbi  44571  abssubrp  45520  cnambpcma  47536