Theorem subcl 11457

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ∃!wreu 3366  ℩crio 7357  (class class class)co 7402  ℂcc 11105   + caddc 11110   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-po 5579  df-so 5580  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-ltxr 11251  df-sub 11444

This theorem is referenced by:  negcl  11458  subf  11460  pncan3  11466  npcan  11467  addsubass  11468  addsub  11469  addsub12  11471  addsubeq4  11473  npncan  11479  nppcan  11480  nnpcan  11481  nppcan3  11482  subcan2  11483  subsub2  11486  subsub4  11491  nnncan  11493  nnncan1  11494  nnncan2  11495  npncan3  11496  addsub4  11501  subadd4  11502  peano2cnm  11524  subcli  11534  subcld  11569  subeqrev  11634  subdi  11645  subdir  11646  mulsub2  11656  recextlem1  11842  recex  11844  mulcan1g  11865  div2sub  12037  cju  12206  halfaddsubcl  12442  halfaddsub  12443  iccf1o  13471  modsumfzodifsn  13907  sersub  14009  sqsubswap  14080  subsq  14172  subsq2  14173  bcn2  14277  pfxccatin12lem1  14676  pfxccatin12lem2  14679  shftval2  15020  2shfti  15025  sqabssub  15228  abssub  15271  abs3dif  15276  abs2dif  15277  abs2difabs  15279  climuni  15494  cjcn2  15542  recn2  15543  imcn2  15544  o1sub  15558  climsub  15576  caucvgr  15620  iseralt  15629  fsum0diag2  15727  arisum2  15805  geoserg  15810  geolim  15814  geolim2  15815  georeclim  15816  geo2sum  15817  geoisum1c  15824  fallfacval2  15953  fallfacval3  15954  fallfaccl  15958  risefallfac  15966  fallfacp1  15972  0fallfac  15979  binomfallfaclem2  15982  bpoly2  15999  bpoly3  16000  fsumcube  16002  tanadd  16109  addsin  16112  fzocongeq  16266  odd2np1  16283  divalglem9  16343  phiprm  16711  pythagtriplem4  16753  pythagtriplem12  16760  pythagtriplem14  16762  pythagtriplem16  16764  fldivp1  16831  4sqlem19  16897  vdwapun  16908  vdwlem6  16920  xrsdsreclb  21278  cnmet  24612  icccvx  24799  reparphti  24847  reparphtiOLD  24848  pcorevlem  24877  cncmet  25174  dveflem  25835  dvef  25836  dv11cn  25858  coeeulem  26080  geolim3  26195  abelthlem2  26288  abelthlem7  26294  efimpi  26345  ptolemy  26350  tangtx  26359  abssinper  26374  cosne0  26382  tanregt0  26392  eflogeq  26455  logneg2  26468  advlogexp  26508  logtayl  26513  logtayl2  26515  ang180lem1  26660  ang180lem2  26661  ang180lem3  26662  lawcos  26667  pythag  26668  isosctrlem1  26669  isosctrlem2  26670  asinlem  26719  asinlem2  26720  asinlem3a  26721  asinlem3  26722  asinf  26723  acosf  26725  atanf  26731  asinneg  26737  efiasin  26739  sinasin  26740  asinsin  26743  acoscos  26744  asinbnd  26750  cosasin  26755  atanneg  26758  atancj  26761  efiatan  26763  atanlogaddlem  26764  atanlogadd  26765  atanlogsublem  26766  atanlogsub  26767  efiatan2  26768  2efiatan  26769  cosatan  26772  atantan  26774  atanbndlem  26776  atans2  26782  dvatan  26786  atantayl  26788  atantayl2  26789  birthdaylem2  26803  scvxcvx  26837  basellem8  26939  1sgm2ppw  27052  logfacbnd3  27075  logfacrlim  27076  perfect1  27080  dchrsum2  27120  sumdchr2  27122  bposlem9  27144  lgsquad2  27238  addsq2reu  27292  rplogsumlem1  27336  dchrmusum2  27346  log2sumbnd  27396  pntrsumo1  27417  brbtwn2  28635  colinearalg  28640  axcgrid  28646  axsegconlem1  28647  ax5seglem1  28658  ax5seglem2  28659  ax5seglem3  28661  ax5seglem5  28663  ax5seglem9  28667  axbtwnid  28669  axeuclidlem  28692  axcontlem2  28695  axcontlem4  28697  axcontlem7  28700  axcontlem8  28701  crctcshwlkn0lem6  29541  eucrctshift  29968  hvmulcan2  30798  subfacp1lem6  34667  cvxsconn  34725  resconn  34728  sinccvglem  35148  sin2h  36972  tan2h  36974  itg2addnclem3  37035  ftc1anclem4  37058  ftc1anclem5  37059  ftc1anclem6  37060  ftc1anclem7  37061  ftc1anc  37063  dvasin  37066  dvacos  37067  lcmineqlem4  41394  lcmineqlem8  41398  rmspecsqrtnq  42158  jm2.17a  42213  acongeq  42236  jm2.27c  42260  lhe4.4ex1a  43602  dvconstbi  43607  abssubrp  44495  cnambpcma  46512