Theorem subcl 11392

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!wreu 3340  ℩crio 7323  (class class class)co 7367  ℂcc 11036   + caddc 11041   − cmin 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379

This theorem is referenced by:  negcl  11393  subf  11395  pncan3  11401  npcan  11402  addsubass  11403  addsub  11404  addsub12  11406  addsubeq4  11408  npncan  11415  nppcan  11416  nnpcan  11417  nppcan3  11418  subcan2  11419  subsub2  11422  subsub4  11427  nnncan  11429  nnncan1  11430  nnncan2  11431  npncan3  11432  addsub4  11437  subadd4  11438  peano2cnm  11460  subcli  11470  subcld  11505  subeqrev  11572  subdi  11583  subdir  11584  mulsub2  11594  recextlem1  11780  recex  11782  mulcan1g  11803  div2sub  11980  cju  12155  halfaddsubcl  12409  halfaddsub  12410  iccf1o  13449  modsumfzodifsn  13906  sersub  14007  sqsubswap  14079  subsq  14172  subsq2  14173  bcn2  14281  pfxccatin12lem1  14690  pfxccatin12lem2  14693  shftval2  15037  2shfti  15042  sqabssub  15245  abssub  15289  abs3dif  15294  abs2dif  15295  abs2difabs  15297  climuni  15514  cjcn2  15562  recn2  15563  imcn2  15564  o1sub  15578  climsub  15596  caucvgr  15638  iseralt  15647  fsum0diag2  15745  arisum2  15826  geoserg  15831  geolim  15835  geolim2  15836  georeclim  15837  geo2sum  15838  geoisum1c  15845  fallfacval2  15976  fallfacval3  15977  fallfaccl  15981  risefallfac  15989  fallfacp1  15995  0fallfac  16002  binomfallfaclem2  16005  bpoly2  16022  bpoly3  16023  fsumcube  16025  tanadd  16134  addsin  16137  fzocongeq  16293  odd2np1  16310  divalglem9  16370  phiprm  16747  pythagtriplem4  16790  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  fldivp1  16868  4sqlem19  16934  vdwapun  16945  vdwlem6  16957  xrsdsreclb  21394  cnmet  24736  icccvx  24917  reparphti  24964  pcorevlem  24993  cncmet  25289  dveflem  25946  dvef  25947  dv11cn  25968  coeeulem  26189  geolim3  26305  abelthlem2  26397  abelthlem7  26403  efimpi  26455  ptolemy  26460  tangtx  26469  abssinper  26485  cosne0  26493  tanregt0  26503  eflogeq  26566  logneg2  26579  advlogexp  26619  logtayl  26624  logtayl2  26626  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  lawcos  26780  pythag  26781  isosctrlem1  26782  isosctrlem2  26783  asinlem  26832  asinlem2  26833  asinlem3a  26834  asinlem3  26835  asinf  26836  acosf  26838  atanf  26844  asinneg  26850  efiasin  26852  sinasin  26853  asinsin  26856  acoscos  26857  asinbnd  26863  cosasin  26868  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsublem  26879  atanlogsub  26880  efiatan2  26881  2efiatan  26882  cosatan  26885  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  atantayl2  26902  birthdaylem2  26916  scvxcvx  26949  basellem8  27051  1sgm2ppw  27163  logfacbnd3  27186  logfacrlim  27187  perfect1  27191  dchrsum2  27231  sumdchr2  27233  bposlem9  27255  lgsquad2  27349  addsq2reu  27403  rplogsumlem1  27447  dchrmusum2  27457  log2sumbnd  27507  pntrsumo1  27528  brbtwn2  28974  colinearalg  28979  axcgrid  28985  axsegconlem1  28986  ax5seglem1  28997  ax5seglem2  28998  ax5seglem3  29000  ax5seglem5  29002  ax5seglem9  29006  axbtwnid  29008  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  crctcshwlkn0lem6  29883  eucrctshift  30313  hvmulcan2  31144  subfacp1lem6  35367  cvxsconn  35425  resconn  35428  sinccvglem  35854  sin2h  37931  tan2h  37933  itg2addnclem3  37994  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  dvasin  38025  dvacos  38026  lcmineqlem4  42471  lcmineqlem8  42475  rmspecsqrtnq  43334  jm2.17a  43388  acongeq  43411  jm2.27c  43435  lhe4.4ex1a  44756  dvconstbi  44761  abssubrp  45709  cnambpcma  47742