Theorem subcl 11383

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 11375	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11374	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 458	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7334	. . 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 7316  (class class class)co 7360  ℂcc 11027   + caddc 11032   − cmin 11368

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 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

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 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370

This theorem is referenced by:  negcl  11384  subf  11386  pncan3  11392  npcan  11393  addsubass  11394  addsub  11395  addsub12  11397  addsubeq4  11399  npncan  11406  nppcan  11407  nnpcan  11408  nppcan3  11409  subcan2  11410  subsub2  11413  subsub4  11418  nnncan  11420  nnncan1  11421  nnncan2  11422  npncan3  11423  addsub4  11428  subadd4  11429  peano2cnm  11451  subcli  11461  subcld  11496  subeqrev  11563  subdi  11574  subdir  11575  mulsub2  11585  recextlem1  11771  recex  11773  mulcan1g  11794  div2sub  11971  cju  12146  halfaddsubcl  12400  halfaddsub  12401  iccf1o  13440  modsumfzodifsn  13897  sersub  13998  sqsubswap  14070  subsq  14163  subsq2  14164  bcn2  14272  pfxccatin12lem1  14681  pfxccatin12lem2  14684  shftval2  15028  2shfti  15033  sqabssub  15236  abssub  15280  abs3dif  15285  abs2dif  15286  abs2difabs  15288  climuni  15505  cjcn2  15553  recn2  15554  imcn2  15555  o1sub  15569  climsub  15587  caucvgr  15629  iseralt  15638  fsum0diag2  15736  arisum2  15817  geoserg  15822  geolim  15826  geolim2  15827  georeclim  15828  geo2sum  15829  geoisum1c  15836  fallfacval2  15967  fallfacval3  15968  fallfaccl  15972  risefallfac  15980  fallfacp1  15986  0fallfac  15993  binomfallfaclem2  15996  bpoly2  16013  bpoly3  16014  fsumcube  16016  tanadd  16125  addsin  16128  fzocongeq  16284  odd2np1  16301  divalglem9  16361  phiprm  16738  pythagtriplem4  16781  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  fldivp1  16859  4sqlem19  16925  vdwapun  16936  vdwlem6  16948  xrsdsreclb  21403  cnmet  24746  icccvx  24927  reparphti  24974  pcorevlem  25003  cncmet  25299  dveflem  25956  dvef  25957  dv11cn  25978  coeeulem  26199  geolim3  26316  abelthlem2  26410  abelthlem7  26416  efimpi  26468  ptolemy  26473  tangtx  26482  abssinper  26498  cosne0  26506  tanregt0  26516  eflogeq  26579  logneg2  26592  advlogexp  26632  logtayl  26637  logtayl2  26639  ang180lem1  26786  ang180lem2  26787  ang180lem3  26788  lawcos  26793  pythag  26794  isosctrlem1  26795  isosctrlem2  26796  asinlem  26845  asinlem2  26846  asinlem3a  26847  asinlem3  26848  asinf  26849  acosf  26851  atanf  26857  asinneg  26863  efiasin  26865  sinasin  26866  asinsin  26869  acoscos  26870  asinbnd  26876  cosasin  26881  atanneg  26884  atancj  26887  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsublem  26892  atanlogsub  26893  efiatan2  26894  2efiatan  26895  cosatan  26898  atantan  26900  atanbndlem  26902  atans2  26908  dvatan  26912  atantayl  26914  atantayl2  26915  birthdaylem2  26929  scvxcvx  26963  basellem8  27065  1sgm2ppw  27177  logfacbnd3  27200  logfacrlim  27201  perfect1  27205  dchrsum2  27245  sumdchr2  27247  bposlem9  27269  lgsquad2  27363  addsq2reu  27417  rplogsumlem1  27461  dchrmusum2  27471  log2sumbnd  27521  pntrsumo1  27542  brbtwn2  28988  colinearalg  28993  axcgrid  28999  axsegconlem1  29000  ax5seglem1  29011  ax5seglem2  29012  ax5seglem3  29014  ax5seglem5  29016  ax5seglem9  29020  axbtwnid  29022  axeuclidlem  29045  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  crctcshwlkn0lem6  29898  eucrctshift  30328  hvmulcan2  31159  subfacp1lem6  35383  cvxsconn  35441  resconn  35444  sinccvglem  35870  sin2h  37945  tan2h  37947  itg2addnclem3  38008  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anc  38036  dvasin  38039  dvacos  38040  lcmineqlem4  42485  lcmineqlem8  42489  rmspecsqrtnq  43352  jm2.17a  43406  acongeq  43429  jm2.27c  43453  lhe4.4ex1a  44774  dvconstbi  44779  abssubrp  45727  cnambpcma  47754