Theorem subcl 11427

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!wreu 3354  ℩crio 7346  (class class class)co 7390  ℂcc 11073   + caddc 11078   − cmin 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  negcl  11428  subf  11430  pncan3  11436  npcan  11437  addsubass  11438  addsub  11439  addsub12  11441  addsubeq4  11443  npncan  11450  nppcan  11451  nnpcan  11452  nppcan3  11453  subcan2  11454  subsub2  11457  subsub4  11462  nnncan  11464  nnncan1  11465  nnncan2  11466  npncan3  11467  addsub4  11472  subadd4  11473  peano2cnm  11495  subcli  11505  subcld  11540  subeqrev  11607  subdi  11618  subdir  11619  mulsub2  11629  recextlem1  11815  recex  11817  mulcan1g  11838  div2sub  12014  cju  12189  halfaddsubcl  12421  halfaddsub  12422  iccf1o  13464  modsumfzodifsn  13916  sersub  14017  sqsubswap  14089  subsq  14182  subsq2  14183  bcn2  14291  pfxccatin12lem1  14700  pfxccatin12lem2  14703  shftval2  15048  2shfti  15053  sqabssub  15256  abssub  15300  abs3dif  15305  abs2dif  15306  abs2difabs  15308  climuni  15525  cjcn2  15573  recn2  15574  imcn2  15575  o1sub  15589  climsub  15607  caucvgr  15649  iseralt  15658  fsum0diag2  15756  arisum2  15834  geoserg  15839  geolim  15843  geolim2  15844  georeclim  15845  geo2sum  15846  geoisum1c  15853  fallfacval2  15984  fallfacval3  15985  fallfaccl  15989  risefallfac  15997  fallfacp1  16003  0fallfac  16010  binomfallfaclem2  16013  bpoly2  16030  bpoly3  16031  fsumcube  16033  tanadd  16142  addsin  16145  fzocongeq  16301  odd2np1  16318  divalglem9  16378  phiprm  16754  pythagtriplem4  16797  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  fldivp1  16875  4sqlem19  16941  vdwapun  16952  vdwlem6  16964  xrsdsreclb  21337  cnmet  24666  icccvx  24855  reparphti  24903  reparphtiOLD  24904  pcorevlem  24933  cncmet  25229  dveflem  25890  dvef  25891  dv11cn  25913  coeeulem  26136  geolim3  26254  abelthlem2  26349  abelthlem7  26355  efimpi  26407  ptolemy  26412  tangtx  26421  abssinper  26437  cosne0  26445  tanregt0  26455  eflogeq  26518  logneg2  26531  advlogexp  26571  logtayl  26576  logtayl2  26578  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  lawcos  26733  pythag  26734  isosctrlem1  26735  isosctrlem2  26736  asinlem  26785  asinlem2  26786  asinlem3a  26787  asinlem3  26788  asinf  26789  acosf  26791  atanf  26797  asinneg  26803  efiasin  26805  sinasin  26806  asinsin  26809  acoscos  26810  asinbnd  26816  cosasin  26821  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  efiatan2  26834  2efiatan  26835  cosatan  26838  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  atantayl2  26855  birthdaylem2  26869  scvxcvx  26903  basellem8  27005  1sgm2ppw  27118  logfacbnd3  27141  logfacrlim  27142  perfect1  27146  dchrsum2  27186  sumdchr2  27188  bposlem9  27210  lgsquad2  27304  addsq2reu  27358  rplogsumlem1  27402  dchrmusum2  27412  log2sumbnd  27462  pntrsumo1  27483  brbtwn2  28839  colinearalg  28844  axcgrid  28850  axsegconlem1  28851  ax5seglem1  28862  ax5seglem2  28863  ax5seglem3  28865  ax5seglem5  28867  ax5seglem9  28871  axbtwnid  28873  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  crctcshwlkn0lem6  29752  eucrctshift  30179  hvmulcan2  31009  subfacp1lem6  35179  cvxsconn  35237  resconn  35240  sinccvglem  35666  sin2h  37611  tan2h  37613  itg2addnclem3  37674  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702  dvasin  37705  dvacos  37706  lcmineqlem4  42027  lcmineqlem8  42031  rmspecsqrtnq  42901  jm2.17a  42956  acongeq  42979  jm2.27c  43003  lhe4.4ex1a  44325  dvconstbi  44330  abssubrp  45281  cnambpcma  47299