Theorem subcl 11391

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

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

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 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  negcl  11392  subf  11394  pncan3  11400  npcan  11401  addsubass  11402  addsub  11403  addsub12  11405  addsubeq4  11407  npncan  11414  nppcan  11415  nnpcan  11416  nppcan3  11417  subcan2  11418  subsub2  11421  subsub4  11426  nnncan  11428  nnncan1  11429  nnncan2  11430  npncan3  11431  addsub4  11436  subadd4  11437  peano2cnm  11459  subcli  11469  subcld  11504  subeqrev  11571  subdi  11582  subdir  11583  mulsub2  11593  recextlem1  11779  recex  11781  mulcan1g  11802  div2sub  11978  cju  12153  halfaddsubcl  12385  halfaddsub  12386  iccf1o  13424  modsumfzodifsn  13879  sersub  13980  sqsubswap  14052  subsq  14145  subsq2  14146  bcn2  14254  pfxccatin12lem1  14663  pfxccatin12lem2  14666  shftval2  15010  2shfti  15015  sqabssub  15218  abssub  15262  abs3dif  15267  abs2dif  15268  abs2difabs  15270  climuni  15487  cjcn2  15535  recn2  15536  imcn2  15537  o1sub  15551  climsub  15569  caucvgr  15611  iseralt  15620  fsum0diag2  15718  arisum2  15796  geoserg  15801  geolim  15805  geolim2  15806  georeclim  15807  geo2sum  15808  geoisum1c  15815  fallfacval2  15946  fallfacval3  15947  fallfaccl  15951  risefallfac  15959  fallfacp1  15965  0fallfac  15972  binomfallfaclem2  15975  bpoly2  15992  bpoly3  15993  fsumcube  15995  tanadd  16104  addsin  16107  fzocongeq  16263  odd2np1  16280  divalglem9  16340  phiprm  16716  pythagtriplem4  16759  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  fldivp1  16837  4sqlem19  16903  vdwapun  16914  vdwlem6  16926  xrsdsreclb  21380  cnmet  24727  icccvx  24916  reparphti  24964  reparphtiOLD  24965  pcorevlem  24994  cncmet  25290  dveflem  25951  dvef  25952  dv11cn  25974  coeeulem  26197  geolim3  26315  abelthlem2  26410  abelthlem7  26416  efimpi  26468  ptolemy  26473  tangtx  26482  abssinper  26498  cosne0  26506  tanregt0  26516  eflogeq  26579  logneg2  26592  advlogexp  26632  logtayl  26637  logtayl2  26639  ang180lem1  26787  ang180lem2  26788  ang180lem3  26789  lawcos  26794  pythag  26795  isosctrlem1  26796  isosctrlem2  26797  asinlem  26846  asinlem2  26847  asinlem3a  26848  asinlem3  26849  asinf  26850  acosf  26852  atanf  26858  asinneg  26864  efiasin  26866  sinasin  26867  asinsin  26870  acoscos  26871  asinbnd  26877  cosasin  26882  atanneg  26885  atancj  26888  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsublem  26893  atanlogsub  26894  efiatan2  26895  2efiatan  26896  cosatan  26899  atantan  26901  atanbndlem  26903  atans2  26909  dvatan  26913  atantayl  26915  atantayl2  26916  birthdaylem2  26930  scvxcvx  26964  basellem8  27066  1sgm2ppw  27179  logfacbnd3  27202  logfacrlim  27203  perfect1  27207  dchrsum2  27247  sumdchr2  27249  bposlem9  27271  lgsquad2  27365  addsq2reu  27419  rplogsumlem1  27463  dchrmusum2  27473  log2sumbnd  27523  pntrsumo1  27544  brbtwn2  28990  colinearalg  28995  axcgrid  29001  axsegconlem1  29002  ax5seglem1  29013  ax5seglem2  29014  ax5seglem3  29016  ax5seglem5  29018  ax5seglem9  29022  axbtwnid  29024  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  crctcshwlkn0lem6  29900  eucrctshift  30330  hvmulcan2  31160  subfacp1lem6  35398  cvxsconn  35456  resconn  35459  sinccvglem  35885  sin2h  37855  tan2h  37857  itg2addnclem3  37918  ftc1anclem4  37941  ftc1anclem5  37942  ftc1anclem6  37943  ftc1anclem7  37944  ftc1anc  37946  dvasin  37949  dvacos  37950  lcmineqlem4  42396  lcmineqlem8  42400  rmspecsqrtnq  43257  jm2.17a  43311  acongeq  43334  jm2.27c  43358  lhe4.4ex1a  44679  dvconstbi  44684  abssubrp  45632  cnambpcma  47648