Theorem subcl 11366

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃!wreu 3345  ℩crio 7308  (class class class)co 7352  ℂcc 11011   + caddc 11016   − cmin 11351

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 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-ltxr 11158  df-sub 11353

This theorem is referenced by:  negcl  11367  subf  11369  pncan3  11375  npcan  11376  addsubass  11377  addsub  11378  addsub12  11380  addsubeq4  11382  npncan  11389  nppcan  11390  nnpcan  11391  nppcan3  11392  subcan2  11393  subsub2  11396  subsub4  11401  nnncan  11403  nnncan1  11404  nnncan2  11405  npncan3  11406  addsub4  11411  subadd4  11412  peano2cnm  11434  subcli  11444  subcld  11479  subeqrev  11546  subdi  11557  subdir  11558  mulsub2  11568  recextlem1  11754  recex  11756  mulcan1g  11777  div2sub  11953  cju  12128  halfaddsubcl  12360  halfaddsub  12361  iccf1o  13398  modsumfzodifsn  13853  sersub  13954  sqsubswap  14026  subsq  14119  subsq2  14120  bcn2  14228  pfxccatin12lem1  14637  pfxccatin12lem2  14640  shftval2  14984  2shfti  14989  sqabssub  15192  abssub  15236  abs3dif  15241  abs2dif  15242  abs2difabs  15244  climuni  15461  cjcn2  15509  recn2  15510  imcn2  15511  o1sub  15525  climsub  15543  caucvgr  15585  iseralt  15594  fsum0diag2  15692  arisum2  15770  geoserg  15775  geolim  15779  geolim2  15780  georeclim  15781  geo2sum  15782  geoisum1c  15789  fallfacval2  15920  fallfacval3  15921  fallfaccl  15925  risefallfac  15933  fallfacp1  15939  0fallfac  15946  binomfallfaclem2  15949  bpoly2  15966  bpoly3  15967  fsumcube  15969  tanadd  16078  addsin  16081  fzocongeq  16237  odd2np1  16254  divalglem9  16314  phiprm  16690  pythagtriplem4  16733  pythagtriplem12  16740  pythagtriplem14  16742  pythagtriplem16  16744  fldivp1  16811  4sqlem19  16877  vdwapun  16888  vdwlem6  16900  xrsdsreclb  21352  cnmet  24687  icccvx  24876  reparphti  24924  reparphtiOLD  24925  pcorevlem  24954  cncmet  25250  dveflem  25911  dvef  25912  dv11cn  25934  coeeulem  26157  geolim3  26275  abelthlem2  26370  abelthlem7  26376  efimpi  26428  ptolemy  26433  tangtx  26442  abssinper  26458  cosne0  26466  tanregt0  26476  eflogeq  26539  logneg2  26552  advlogexp  26592  logtayl  26597  logtayl2  26599  ang180lem1  26747  ang180lem2  26748  ang180lem3  26749  lawcos  26754  pythag  26755  isosctrlem1  26756  isosctrlem2  26757  asinlem  26806  asinlem2  26807  asinlem3a  26808  asinlem3  26809  asinf  26810  acosf  26812  atanf  26818  asinneg  26824  efiasin  26826  sinasin  26827  asinsin  26830  acoscos  26831  asinbnd  26837  cosasin  26842  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atanlogsub  26854  efiatan2  26855  2efiatan  26856  cosatan  26859  atantan  26861  atanbndlem  26863  atans2  26869  dvatan  26873  atantayl  26875  atantayl2  26876  birthdaylem2  26890  scvxcvx  26924  basellem8  27026  1sgm2ppw  27139  logfacbnd3  27162  logfacrlim  27163  perfect1  27167  dchrsum2  27207  sumdchr2  27209  bposlem9  27231  lgsquad2  27325  addsq2reu  27379  rplogsumlem1  27423  dchrmusum2  27433  log2sumbnd  27483  pntrsumo1  27504  brbtwn2  28885  colinearalg  28890  axcgrid  28896  axsegconlem1  28897  ax5seglem1  28908  ax5seglem2  28909  ax5seglem3  28911  ax5seglem5  28913  ax5seglem9  28917  axbtwnid  28919  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  crctcshwlkn0lem6  29795  eucrctshift  30225  hvmulcan2  31055  subfacp1lem6  35250  cvxsconn  35308  resconn  35311  sinccvglem  35737  sin2h  37671  tan2h  37673  itg2addnclem3  37734  ftc1anclem4  37757  ftc1anclem5  37758  ftc1anclem6  37759  ftc1anclem7  37760  ftc1anc  37762  dvasin  37765  dvacos  37766  lcmineqlem4  42146  lcmineqlem8  42150  rmspecsqrtnq  43024  jm2.17a  43078  acongeq  43101  jm2.27c  43125  lhe4.4ex1a  44447  dvconstbi  44452  abssubrp  45402  cnambpcma  47419