Theorem subcl 11456

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 11448	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11447	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 460	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7380	. . 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 7361  (class class class)co 7406  ℂcc 11105   + caddc 11110   − cmin 11441

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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  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 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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-ltxr 11250  df-sub 11443

This theorem is referenced by:  negcl  11457  subf  11459  pncan3  11465  npcan  11466  addsubass  11467  addsub  11468  addsub12  11470  addsubeq4  11472  npncan  11478  nppcan  11479  nnpcan  11480  nppcan3  11481  subcan2  11482  subsub2  11485  subsub4  11490  nnncan  11492  nnncan1  11493  nnncan2  11494  npncan3  11495  addsub4  11500  subadd4  11501  peano2cnm  11523  subcli  11533  subcld  11568  subeqrev  11633  subdi  11644  subdir  11645  mulsub2  11655  recextlem1  11841  recex  11843  mulcan1g  11864  div2sub  12036  cju  12205  halfaddsubcl  12441  halfaddsub  12442  iccf1o  13470  modsumfzodifsn  13906  sersub  14008  sqsubswap  14079  subsq  14171  subsq2  14172  bcn2  14276  pfxccatin12lem1  14675  pfxccatin12lem2  14678  shftval2  15019  2shfti  15024  sqabssub  15227  abssub  15270  abs3dif  15275  abs2dif  15276  abs2difabs  15278  climuni  15493  cjcn2  15541  recn2  15542  imcn2  15543  o1sub  15557  climsub  15575  caucvgr  15619  iseralt  15628  fsum0diag2  15726  arisum2  15804  geoserg  15809  geolim  15813  geolim2  15814  georeclim  15815  geo2sum  15816  geoisum1c  15823  fallfacval2  15952  fallfacval3  15953  fallfaccl  15957  risefallfac  15965  fallfacp1  15971  0fallfac  15978  binomfallfaclem2  15981  bpoly2  15998  bpoly3  15999  fsumcube  16001  tanadd  16107  addsin  16110  fzocongeq  16264  odd2np1  16281  divalglem9  16341  phiprm  16707  pythagtriplem4  16749  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  fldivp1  16827  4sqlem19  16893  vdwapun  16904  vdwlem6  16916  xrsdsreclb  20985  cnmet  24280  icccvx  24458  reparphti  24505  pcorevlem  24534  cncmet  24831  dveflem  25488  dvef  25489  dv11cn  25510  coeeulem  25730  geolim3  25844  abelthlem2  25936  abelthlem7  25942  efimpi  25993  ptolemy  25998  tangtx  26007  abssinper  26022  cosne0  26030  tanregt0  26040  eflogeq  26102  logneg2  26115  advlogexp  26155  logtayl  26160  logtayl2  26162  ang180lem1  26304  ang180lem2  26305  ang180lem3  26306  lawcos  26311  pythag  26312  isosctrlem1  26313  isosctrlem2  26314  asinlem  26363  asinlem2  26364  asinlem3a  26365  asinlem3  26366  asinf  26367  acosf  26369  atanf  26375  asinneg  26381  efiasin  26383  sinasin  26384  asinsin  26387  acoscos  26388  asinbnd  26394  cosasin  26399  atanneg  26402  atancj  26405  efiatan  26407  atanlogaddlem  26408  atanlogadd  26409  atanlogsublem  26410  atanlogsub  26411  efiatan2  26412  2efiatan  26413  cosatan  26416  atantan  26418  atanbndlem  26420  atans2  26426  dvatan  26430  atantayl  26432  atantayl2  26433  birthdaylem2  26447  scvxcvx  26480  basellem8  26582  1sgm2ppw  26693  logfacbnd3  26716  logfacrlim  26717  perfect1  26721  dchrsum2  26761  sumdchr2  26763  bposlem9  26785  lgsquad2  26879  addsq2reu  26933  rplogsumlem1  26977  dchrmusum2  26987  log2sumbnd  27037  pntrsumo1  27058  brbtwn2  28153  colinearalg  28158  axcgrid  28164  axsegconlem1  28165  ax5seglem1  28176  ax5seglem2  28177  ax5seglem3  28179  ax5seglem5  28181  ax5seglem9  28185  axbtwnid  28187  axeuclidlem  28210  axcontlem2  28213  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  crctcshwlkn0lem6  29059  eucrctshift  29486  hvmulcan2  30314  subfacp1lem6  34165  cvxsconn  34223  resconn  34226  sinccvglem  34646  gg-reparphti  35161  sin2h  36467  tan2h  36469  itg2addnclem3  36530  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anc  36558  dvasin  36561  dvacos  36562  lcmineqlem4  40886  lcmineqlem8  40890  rmspecsqrtnq  41630  jm2.17a  41685  acongeq  41708  jm2.27c  41732  lhe4.4ex1a  43074  dvconstbi  43079  abssubrp  43972  cnambpcma  45989