Theorem subcl 11380

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!wreu 3341  ℩crio 7314  (class class class)co 7358  ℂcc 11025   + caddc 11030   − cmin 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172  df-sub 11367

This theorem is referenced by:  negcl  11381  subf  11383  pncan3  11389  npcan  11390  addsubass  11391  addsub  11392  addsub12  11394  addsubeq4  11396  npncan  11403  nppcan  11404  nnpcan  11405  nppcan3  11406  subcan2  11407  subsub2  11410  subsub4  11415  nnncan  11417  nnncan1  11418  nnncan2  11419  npncan3  11420  addsub4  11425  subadd4  11426  peano2cnm  11448  subcli  11458  subcld  11493  subeqrev  11560  subdi  11571  subdir  11572  mulsub2  11582  recextlem1  11768  recex  11770  mulcan1g  11791  div2sub  11967  cju  12142  halfaddsubcl  12374  halfaddsub  12375  iccf1o  13413  modsumfzodifsn  13868  sersub  13969  sqsubswap  14041  subsq  14134  subsq2  14135  bcn2  14243  pfxccatin12lem1  14652  pfxccatin12lem2  14655  shftval2  14999  2shfti  15004  sqabssub  15207  abssub  15251  abs3dif  15256  abs2dif  15257  abs2difabs  15259  climuni  15476  cjcn2  15524  recn2  15525  imcn2  15526  o1sub  15540  climsub  15558  caucvgr  15600  iseralt  15609  fsum0diag2  15707  arisum2  15785  geoserg  15790  geolim  15794  geolim2  15795  georeclim  15796  geo2sum  15797  geoisum1c  15804  fallfacval2  15935  fallfacval3  15936  fallfaccl  15940  risefallfac  15948  fallfacp1  15954  0fallfac  15961  binomfallfaclem2  15964  bpoly2  15981  bpoly3  15982  fsumcube  15984  tanadd  16093  addsin  16096  fzocongeq  16252  odd2np1  16269  divalglem9  16329  phiprm  16705  pythagtriplem4  16748  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem16  16759  fldivp1  16826  4sqlem19  16892  vdwapun  16903  vdwlem6  16915  xrsdsreclb  21370  cnmet  24714  icccvx  24895  reparphti  24942  pcorevlem  24971  cncmet  25267  dveflem  25924  dvef  25925  dv11cn  25947  coeeulem  26170  geolim3  26287  abelthlem2  26382  abelthlem7  26388  efimpi  26440  ptolemy  26445  tangtx  26454  abssinper  26470  cosne0  26478  tanregt0  26488  eflogeq  26551  logneg2  26564  advlogexp  26604  logtayl  26609  logtayl2  26611  ang180lem1  26759  ang180lem2  26760  ang180lem3  26761  lawcos  26766  pythag  26767  isosctrlem1  26768  isosctrlem2  26769  asinlem  26818  asinlem2  26819  asinlem3a  26820  asinlem3  26821  asinf  26822  acosf  26824  atanf  26830  asinneg  26836  efiasin  26838  sinasin  26839  asinsin  26842  acoscos  26843  asinbnd  26849  cosasin  26854  atanneg  26857  atancj  26860  efiatan  26862  atanlogaddlem  26863  atanlogadd  26864  atanlogsublem  26865  atanlogsub  26866  efiatan2  26867  2efiatan  26868  cosatan  26871  atantan  26873  atanbndlem  26875  atans2  26881  dvatan  26885  atantayl  26887  atantayl2  26888  birthdaylem2  26902  scvxcvx  26936  basellem8  27038  1sgm2ppw  27151  logfacbnd3  27174  logfacrlim  27175  perfect1  27179  dchrsum2  27219  sumdchr2  27221  bposlem9  27243  lgsquad2  27337  addsq2reu  27391  rplogsumlem1  27435  dchrmusum2  27445  log2sumbnd  27495  pntrsumo1  27516  brbtwn2  28962  colinearalg  28967  axcgrid  28973  axsegconlem1  28974  ax5seglem1  28985  ax5seglem2  28986  ax5seglem3  28988  ax5seglem5  28990  ax5seglem9  28994  axbtwnid  28996  axeuclidlem  29019  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  axcontlem8  29028  crctcshwlkn0lem6  29872  eucrctshift  30302  hvmulcan2  31133  subfacp1lem6  35373  cvxsconn  35431  resconn  35434  sinccvglem  35860  sin2h  37922  tan2h  37924  itg2addnclem3  37985  ftc1anclem4  38008  ftc1anclem5  38009  ftc1anclem6  38010  ftc1anclem7  38011  ftc1anc  38013  dvasin  38016  dvacos  38017  lcmineqlem4  42463  lcmineqlem8  42467  rmspecsqrtnq  43337  jm2.17a  43391  acongeq  43414  jm2.27c  43438  lhe4.4ex1a  44759  dvconstbi  44764  abssubrp  45712  cnambpcma  47728