Theorem subcl 11444

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 11436	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11435	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 463	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7374	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 18	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2865	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∃!wreu 3368  ℩crio 7356  (class class class)co 7400  ℂcc 11086   + caddc 11091   − cmin 11429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236  df-sub 11431

This theorem is referenced by:  negcl  11445  subf  11447  pncan3  11453  npcan  11454  addsubass  11455  addsub  11456  addsub12  11458  addsubeq4  11460  npncan  11467  nppcan  11468  nnpcan  11469  nppcan3  11470  subcan2  11471  subsub2  11474  subsub4  11479  nnncan  11481  nnncan1  11482  nnncan2  11483  npncan3  11484  addsub4  11489  subadd4  11490  peano2cnm  11512  subcli  11522  subcld  11557  subeqrev  11624  subdi  11635  subdir  11636  mulsub2  11646  recextlem1  11832  recex  11834  mulcan1g  11855  div2sub  12031  cju  12205  halfaddsubcl  12467  halfaddsub  12468  iccf1o  13514  modsumfzodifsn  13971  sersub  14072  sqsubswap  14144  subsq  14237  subsq2  14238  bcn2  14346  pfxccatin12lem1  14755  pfxccatin12lem2  14758  shftval2  15102  2shfti  15107  sqabssub  15324  abssub  15368  abs3dif  15373  abs2dif  15374  abs2difabs  15376  climuni  15593  cjcn2  15641  recn2  15642  imcn2  15643  o1sub  15657  climsub  15675  caucvgr  15717  iseralt  15726  fsum0diag2  15824  arisum2  15905  geoserg  15910  geolim  15914  geolim2  15915  georeclim  15916  geo2sum  15917  geoisum1c  15924  fallfacval2  16055  fallfacval3  16056  fallfaccl  16060  risefallfac  16068  fallfacp1  16074  0fallfac  16081  binomfallfaclem2  16084  bpoly2  16101  bpoly3  16102  fsumcube  16104  tanadd  16213  addsin  16216  fzocongeq  16372  odd2np1  16389  divalglem9  16449  phiprm  16826  pythagtriplem4  16869  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem16  16880  fldivp1  16947  4sqlem19  17013  vdwapun  17024  vdwlem6  17036  xrsdsreclb  21524  cnmet  24889  icccvx  25070  reparphti  25117  pcorevlem  25146  cncmet  25442  dveflem  26099  dvef  26100  dv11cn  26121  coeeulem  26342  geolim3  26461  abelthlem2  26553  abelthlem7  26559  efimpi  26614  ptolemy  26619  tangtx  26628  abssinper  26644  cosne0  26652  tanregt0  26662  eflogeq  26725  logneg2  26738  advlogexp  26778  logtayl  26783  logtayl2  26785  ang180lem1  26932  ang180lem2  26933  ang180lem3  26934  lawcos  26939  pythag  26940  isosctrlem1  26941  isosctrlem2  26942  asinlem  26991  asinlem2  26992  asinlem3a  26993  asinlem3  26994  asinf  26995  acosf  26997  atanf  27003  asinneg  27009  efiasin  27011  sinasin  27012  asinsin  27015  acoscos  27016  asinbnd  27022  cosasin  27027  atanneg  27030  atancj  27033  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsublem  27038  atanlogsub  27039  efiatan2  27040  2efiatan  27041  cosatan  27044  atantan  27046  atanbndlem  27048  atans2  27054  dvatan  27058  atantayl  27060  atantayl2  27061  birthdaylem2  27075  scvxcvx  27108  basellem8  27210  1sgm2ppw  27322  logfacbnd3  27345  logfacrlim  27346  perfect1  27350  dchrsum2  27390  sumdchr2  27392  bposlem9  27414  lgsquad2  27508  addsq2reu  27562  rplogsumlem1  27606  dchrmusum2  27616  log2sumbnd  27666  pntrsumo1  27687  brbtwn2  29164  colinearalg  29169  axcgrid  29175  axsegconlem1  29176  ax5seglem1  29187  ax5seglem2  29188  ax5seglem3  29190  ax5seglem5  29192  ax5seglem9  29196  axbtwnid  29198  axeuclidlem  29221  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  axcontlem8  29230  crctcshwlkn0lem6  30073  eucrctshift  30503  hvmulcan2  31334  subfacp1lem6  35548  cvxsconn  35606  resconn  35609  sinccvglem  36035  sin2h  38121  tan2h  38123  itg2addnclem3  38184  ftc1anclem4  38207  ftc1anclem5  38208  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anc  38212  dvasin  38215  dvacos  38216  lcmineqlem4  42661  lcmineqlem8  42665  rmspecsqrtnq  43495  jm2.17a  43549  acongeq  43572  jm2.27c  43596  lhe4.4ex1a  44903  dvconstbi  44908  abssubrp  45853  cnambpcma  47886