Theorem subcl 11420

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!wreu 3352  ℩crio 7343  (class class class)co 7387  ℂcc 11066   + caddc 11071   − cmin 11405

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407

This theorem is referenced by:  negcl  11421  subf  11423  pncan3  11429  npcan  11430  addsubass  11431  addsub  11432  addsub12  11434  addsubeq4  11436  npncan  11443  nppcan  11444  nnpcan  11445  nppcan3  11446  subcan2  11447  subsub2  11450  subsub4  11455  nnncan  11457  nnncan1  11458  nnncan2  11459  npncan3  11460  addsub4  11465  subadd4  11466  peano2cnm  11488  subcli  11498  subcld  11533  subeqrev  11600  subdi  11611  subdir  11612  mulsub2  11622  recextlem1  11808  recex  11810  mulcan1g  11831  div2sub  12007  cju  12182  halfaddsubcl  12414  halfaddsub  12415  iccf1o  13457  modsumfzodifsn  13909  sersub  14010  sqsubswap  14082  subsq  14175  subsq2  14176  bcn2  14284  pfxccatin12lem1  14693  pfxccatin12lem2  14696  shftval2  15041  2shfti  15046  sqabssub  15249  abssub  15293  abs3dif  15298  abs2dif  15299  abs2difabs  15301  climuni  15518  cjcn2  15566  recn2  15567  imcn2  15568  o1sub  15582  climsub  15600  caucvgr  15642  iseralt  15651  fsum0diag2  15749  arisum2  15827  geoserg  15832  geolim  15836  geolim2  15837  georeclim  15838  geo2sum  15839  geoisum1c  15846  fallfacval2  15977  fallfacval3  15978  fallfaccl  15982  risefallfac  15990  fallfacp1  15996  0fallfac  16003  binomfallfaclem2  16006  bpoly2  16023  bpoly3  16024  fsumcube  16026  tanadd  16135  addsin  16138  fzocongeq  16294  odd2np1  16311  divalglem9  16371  phiprm  16747  pythagtriplem4  16790  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  fldivp1  16868  4sqlem19  16934  vdwapun  16945  vdwlem6  16957  xrsdsreclb  21330  cnmet  24659  icccvx  24848  reparphti  24896  reparphtiOLD  24897  pcorevlem  24926  cncmet  25222  dveflem  25883  dvef  25884  dv11cn  25906  coeeulem  26129  geolim3  26247  abelthlem2  26342  abelthlem7  26348  efimpi  26400  ptolemy  26405  tangtx  26414  abssinper  26430  cosne0  26438  tanregt0  26448  eflogeq  26511  logneg2  26524  advlogexp  26564  logtayl  26569  logtayl2  26571  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  lawcos  26726  pythag  26727  isosctrlem1  26728  isosctrlem2  26729  asinlem  26778  asinlem2  26779  asinlem3a  26780  asinlem3  26781  asinf  26782  acosf  26784  atanf  26790  asinneg  26796  efiasin  26798  sinasin  26799  asinsin  26802  acoscos  26803  asinbnd  26809  cosasin  26814  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  efiatan2  26827  2efiatan  26828  cosatan  26831  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  atantayl2  26848  birthdaylem2  26862  scvxcvx  26896  basellem8  26998  1sgm2ppw  27111  logfacbnd3  27134  logfacrlim  27135  perfect1  27139  dchrsum2  27179  sumdchr2  27181  bposlem9  27203  lgsquad2  27297  addsq2reu  27351  rplogsumlem1  27395  dchrmusum2  27405  log2sumbnd  27455  pntrsumo1  27476  brbtwn2  28832  colinearalg  28837  axcgrid  28843  axsegconlem1  28844  ax5seglem1  28855  ax5seglem2  28856  ax5seglem3  28858  ax5seglem5  28860  ax5seglem9  28864  axbtwnid  28866  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  crctcshwlkn0lem6  29745  eucrctshift  30172  hvmulcan2  31002  subfacp1lem6  35172  cvxsconn  35230  resconn  35233  sinccvglem  35659  sin2h  37604  tan2h  37606  itg2addnclem3  37667  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  dvasin  37698  dvacos  37699  lcmineqlem4  42020  lcmineqlem8  42024  rmspecsqrtnq  42894  jm2.17a  42949  acongeq  42972  jm2.27c  42996  lhe4.4ex1a  44318  dvconstbi  44323  abssubrp  45274  cnambpcma  47295