Theorem subcl 11390

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 11382	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11381	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 459	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7337	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2840	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃!wreu 3343  ℩crio 7319  (class class class)co 7363  ℂcc 11034   + caddc 11039   − cmin 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182  df-sub 11377

This theorem is referenced by:  negcl  11391  subf  11393  pncan3  11399  npcan  11400  addsubass  11401  addsub  11402  addsub12  11404  addsubeq4  11406  npncan  11413  nppcan  11414  nnpcan  11415  nppcan3  11416  subcan2  11417  subsub2  11420  subsub4  11425  nnncan  11427  nnncan1  11428  nnncan2  11429  npncan3  11430  addsub4  11435  subadd4  11436  peano2cnm  11458  subcli  11468  subcld  11503  subeqrev  11570  subdi  11581  subdir  11582  mulsub2  11592  recextlem1  11778  recex  11780  mulcan1g  11801  div2sub  11978  cju  12153  halfaddsubcl  12407  halfaddsub  12408  iccf1o  13447  modsumfzodifsn  13904  sersub  14005  sqsubswap  14077  subsq  14170  subsq2  14171  bcn2  14279  pfxccatin12lem1  14688  pfxccatin12lem2  14691  shftval2  15035  2shfti  15040  sqabssub  15243  abssub  15287  abs3dif  15292  abs2dif  15293  abs2difabs  15295  climuni  15512  cjcn2  15560  recn2  15561  imcn2  15562  o1sub  15576  climsub  15594  caucvgr  15636  iseralt  15645  fsum0diag2  15743  arisum2  15824  geoserg  15829  geolim  15833  geolim2  15834  georeclim  15835  geo2sum  15836  geoisum1c  15843  fallfacval2  15974  fallfacval3  15975  fallfaccl  15979  risefallfac  15987  fallfacp1  15993  0fallfac  16000  binomfallfaclem2  16003  bpoly2  16020  bpoly3  16021  fsumcube  16023  tanadd  16132  addsin  16135  fzocongeq  16291  odd2np1  16308  divalglem9  16368  phiprm  16745  pythagtriplem4  16788  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem16  16799  fldivp1  16866  4sqlem19  16932  vdwapun  16943  vdwlem6  16955  xrsdsreclb  21396  cnmet  24761  icccvx  24942  reparphti  24989  pcorevlem  25018  cncmet  25314  dveflem  25971  dvef  25972  dv11cn  25993  coeeulem  26214  geolim3  26330  abelthlem2  26422  abelthlem7  26428  efimpi  26480  ptolemy  26485  tangtx  26494  abssinper  26510  cosne0  26518  tanregt0  26528  eflogeq  26591  logneg2  26604  advlogexp  26644  logtayl  26649  logtayl2  26651  ang180lem1  26798  ang180lem2  26799  ang180lem3  26800  lawcos  26805  pythag  26806  isosctrlem1  26807  isosctrlem2  26808  asinlem  26857  asinlem2  26858  asinlem3a  26859  asinlem3  26860  asinf  26861  acosf  26863  atanf  26869  asinneg  26875  efiasin  26877  sinasin  26878  asinsin  26881  acoscos  26882  asinbnd  26888  cosasin  26893  atanneg  26896  atancj  26899  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsublem  26904  atanlogsub  26905  efiatan2  26906  2efiatan  26907  cosatan  26910  atantan  26912  atanbndlem  26914  atans2  26920  dvatan  26924  atantayl  26926  atantayl2  26927  birthdaylem2  26941  scvxcvx  26974  basellem8  27076  1sgm2ppw  27188  logfacbnd3  27211  logfacrlim  27212  perfect1  27216  dchrsum2  27256  sumdchr2  27258  bposlem9  27280  lgsquad2  27374  addsq2reu  27428  rplogsumlem1  27472  dchrmusum2  27482  log2sumbnd  27532  pntrsumo1  27553  brbtwn2  28999  colinearalg  29004  axcgrid  29010  axsegconlem1  29011  ax5seglem1  29022  ax5seglem2  29023  ax5seglem3  29025  ax5seglem5  29027  ax5seglem9  29031  axbtwnid  29033  axeuclidlem  29056  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  axcontlem8  29065  crctcshwlkn0lem6  29908  eucrctshift  30338  hvmulcan2  31169  subfacp1lem6  35420  cvxsconn  35478  resconn  35481  sinccvglem  35907  sin2h  37984  tan2h  37986  itg2addnclem3  38047  ftc1anclem4  38070  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anc  38075  dvasin  38078  dvacos  38079  lcmineqlem4  42524  lcmineqlem8  42528  rmspecsqrtnq  43358  jm2.17a  43412  acongeq  43435  jm2.27c  43459  lhe4.4ex1a  44780  dvconstbi  44785  abssubrp  45731  cnambpcma  47764