Theorem subcl 11459

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 11451	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11450	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 460	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7383	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2834	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃!wreu 3375  ℩crio 7364  (class class class)co 7409  ℂcc 11108   + caddc 11113   − cmin 11444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253  df-sub 11446

This theorem is referenced by:  negcl  11460  subf  11462  pncan3  11468  npcan  11469  addsubass  11470  addsub  11471  addsub12  11473  addsubeq4  11475  npncan  11481  nppcan  11482  nnpcan  11483  nppcan3  11484  subcan2  11485  subsub2  11488  subsub4  11493  nnncan  11495  nnncan1  11496  nnncan2  11497  npncan3  11498  addsub4  11503  subadd4  11504  peano2cnm  11526  subcli  11536  subcld  11571  subeqrev  11636  subdi  11647  subdir  11648  mulsub2  11658  recextlem1  11844  recex  11846  mulcan1g  11867  div2sub  12039  cju  12208  halfaddsubcl  12444  halfaddsub  12445  iccf1o  13473  modsumfzodifsn  13909  sersub  14011  sqsubswap  14082  subsq  14174  subsq2  14175  bcn2  14279  pfxccatin12lem1  14678  pfxccatin12lem2  14681  shftval2  15022  2shfti  15027  sqabssub  15230  abssub  15273  abs3dif  15278  abs2dif  15279  abs2difabs  15281  climuni  15496  cjcn2  15544  recn2  15545  imcn2  15546  o1sub  15560  climsub  15578  caucvgr  15622  iseralt  15631  fsum0diag2  15729  arisum2  15807  geoserg  15812  geolim  15816  geolim2  15817  georeclim  15818  geo2sum  15819  geoisum1c  15826  fallfacval2  15955  fallfacval3  15956  fallfaccl  15960  risefallfac  15968  fallfacp1  15974  0fallfac  15981  binomfallfaclem2  15984  bpoly2  16001  bpoly3  16002  fsumcube  16004  tanadd  16110  addsin  16113  fzocongeq  16267  odd2np1  16284  divalglem9  16344  phiprm  16710  pythagtriplem4  16752  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  fldivp1  16830  4sqlem19  16896  vdwapun  16907  vdwlem6  16919  xrsdsreclb  20992  cnmet  24288  icccvx  24466  reparphti  24513  pcorevlem  24542  cncmet  24839  dveflem  25496  dvef  25497  dv11cn  25518  coeeulem  25738  geolim3  25852  abelthlem2  25944  abelthlem7  25950  efimpi  26001  ptolemy  26006  tangtx  26015  abssinper  26030  cosne0  26038  tanregt0  26048  eflogeq  26110  logneg2  26123  advlogexp  26163  logtayl  26168  logtayl2  26170  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  lawcos  26321  pythag  26322  isosctrlem1  26323  isosctrlem2  26324  asinlem  26373  asinlem2  26374  asinlem3a  26375  asinlem3  26376  asinf  26377  acosf  26379  atanf  26385  asinneg  26391  efiasin  26393  sinasin  26394  asinsin  26397  acoscos  26398  asinbnd  26404  cosasin  26409  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atanlogsub  26421  efiatan2  26422  2efiatan  26423  cosatan  26426  atantan  26428  atanbndlem  26430  atans2  26436  dvatan  26440  atantayl  26442  atantayl2  26443  birthdaylem2  26457  scvxcvx  26490  basellem8  26592  1sgm2ppw  26703  logfacbnd3  26726  logfacrlim  26727  perfect1  26731  dchrsum2  26771  sumdchr2  26773  bposlem9  26795  lgsquad2  26889  addsq2reu  26943  rplogsumlem1  26987  dchrmusum2  26997  log2sumbnd  27047  pntrsumo1  27068  brbtwn2  28194  colinearalg  28199  axcgrid  28205  axsegconlem1  28206  ax5seglem1  28217  ax5seglem2  28218  ax5seglem3  28220  ax5seglem5  28222  ax5seglem9  28226  axbtwnid  28228  axeuclidlem  28251  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  crctcshwlkn0lem6  29100  eucrctshift  29527  hvmulcan2  30357  subfacp1lem6  34207  cvxsconn  34265  resconn  34268  sinccvglem  34688  gg-reparphti  35203  sin2h  36526  tan2h  36528  itg2addnclem3  36589  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anc  36617  dvasin  36620  dvacos  36621  lcmineqlem4  40945  lcmineqlem8  40949  rmspecsqrtnq  41692  jm2.17a  41747  acongeq  41770  jm2.27c  41794  lhe4.4ex1a  43136  dvconstbi  43141  abssubrp  44033  cnambpcma  46050