Theorem subcl 11359

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃!wreu 3344  ℩crio 7302  (class class class)co 7346  ℂcc 11004   + caddc 11009   − cmin 11344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-sub 11346

This theorem is referenced by:  negcl  11360  subf  11362  pncan3  11368  npcan  11369  addsubass  11370  addsub  11371  addsub12  11373  addsubeq4  11375  npncan  11382  nppcan  11383  nnpcan  11384  nppcan3  11385  subcan2  11386  subsub2  11389  subsub4  11394  nnncan  11396  nnncan1  11397  nnncan2  11398  npncan3  11399  addsub4  11404  subadd4  11405  peano2cnm  11427  subcli  11437  subcld  11472  subeqrev  11539  subdi  11550  subdir  11551  mulsub2  11561  recextlem1  11747  recex  11749  mulcan1g  11770  div2sub  11946  cju  12121  halfaddsubcl  12353  halfaddsub  12354  iccf1o  13396  modsumfzodifsn  13851  sersub  13952  sqsubswap  14024  subsq  14117  subsq2  14118  bcn2  14226  pfxccatin12lem1  14635  pfxccatin12lem2  14638  shftval2  14982  2shfti  14987  sqabssub  15190  abssub  15234  abs3dif  15239  abs2dif  15240  abs2difabs  15242  climuni  15459  cjcn2  15507  recn2  15508  imcn2  15509  o1sub  15523  climsub  15541  caucvgr  15583  iseralt  15592  fsum0diag2  15690  arisum2  15768  geoserg  15773  geolim  15777  geolim2  15778  georeclim  15779  geo2sum  15780  geoisum1c  15787  fallfacval2  15918  fallfacval3  15919  fallfaccl  15923  risefallfac  15931  fallfacp1  15937  0fallfac  15944  binomfallfaclem2  15947  bpoly2  15964  bpoly3  15965  fsumcube  15967  tanadd  16076  addsin  16079  fzocongeq  16235  odd2np1  16252  divalglem9  16312  phiprm  16688  pythagtriplem4  16731  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  fldivp1  16809  4sqlem19  16875  vdwapun  16886  vdwlem6  16898  xrsdsreclb  21351  cnmet  24687  icccvx  24876  reparphti  24924  reparphtiOLD  24925  pcorevlem  24954  cncmet  25250  dveflem  25911  dvef  25912  dv11cn  25934  coeeulem  26157  geolim3  26275  abelthlem2  26370  abelthlem7  26376  efimpi  26428  ptolemy  26433  tangtx  26442  abssinper  26458  cosne0  26466  tanregt0  26476  eflogeq  26539  logneg2  26552  advlogexp  26592  logtayl  26597  logtayl2  26599  ang180lem1  26747  ang180lem2  26748  ang180lem3  26749  lawcos  26754  pythag  26755  isosctrlem1  26756  isosctrlem2  26757  asinlem  26806  asinlem2  26807  asinlem3a  26808  asinlem3  26809  asinf  26810  acosf  26812  atanf  26818  asinneg  26824  efiasin  26826  sinasin  26827  asinsin  26830  acoscos  26831  asinbnd  26837  cosasin  26842  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atanlogsub  26854  efiatan2  26855  2efiatan  26856  cosatan  26859  atantan  26861  atanbndlem  26863  atans2  26869  dvatan  26873  atantayl  26875  atantayl2  26876  birthdaylem2  26890  scvxcvx  26924  basellem8  27026  1sgm2ppw  27139  logfacbnd3  27162  logfacrlim  27163  perfect1  27167  dchrsum2  27207  sumdchr2  27209  bposlem9  27231  lgsquad2  27325  addsq2reu  27379  rplogsumlem1  27423  dchrmusum2  27433  log2sumbnd  27483  pntrsumo1  27504  brbtwn2  28884  colinearalg  28889  axcgrid  28895  axsegconlem1  28896  ax5seglem1  28907  ax5seglem2  28908  ax5seglem3  28910  ax5seglem5  28912  ax5seglem9  28916  axbtwnid  28918  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  crctcshwlkn0lem6  29794  eucrctshift  30221  hvmulcan2  31051  subfacp1lem6  35227  cvxsconn  35285  resconn  35288  sinccvglem  35714  sin2h  37656  tan2h  37658  itg2addnclem3  37719  ftc1anclem4  37742  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anc  37747  dvasin  37750  dvacos  37751  lcmineqlem4  42071  lcmineqlem8  42075  rmspecsqrtnq  42945  jm2.17a  42999  acongeq  43022  jm2.27c  43046  lhe4.4ex1a  44368  dvconstbi  44373  abssubrp  45323  cnambpcma  47331