Theorem subcl 11504

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃!wreu 3375  ℩crio 7386  (class class class)co 7430  ℂcc 11150   + caddc 11155   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491

This theorem is referenced by:  negcl  11505  subf  11507  pncan3  11513  npcan  11514  addsubass  11515  addsub  11516  addsub12  11518  addsubeq4  11520  npncan  11527  nppcan  11528  nnpcan  11529  nppcan3  11530  subcan2  11531  subsub2  11534  subsub4  11539  nnncan  11541  nnncan1  11542  nnncan2  11543  npncan3  11544  addsub4  11549  subadd4  11550  peano2cnm  11572  subcli  11582  subcld  11617  subeqrev  11682  subdi  11693  subdir  11694  mulsub2  11704  recextlem1  11890  recex  11892  mulcan1g  11913  div2sub  12089  cju  12259  halfaddsubcl  12495  halfaddsub  12496  iccf1o  13532  modsumfzodifsn  13981  sersub  14082  sqsubswap  14153  subsq  14245  subsq2  14246  bcn2  14354  pfxccatin12lem1  14762  pfxccatin12lem2  14765  shftval2  15110  2shfti  15115  sqabssub  15318  abssub  15361  abs3dif  15366  abs2dif  15367  abs2difabs  15369  climuni  15584  cjcn2  15632  recn2  15633  imcn2  15634  o1sub  15648  climsub  15666  caucvgr  15708  iseralt  15717  fsum0diag2  15815  arisum2  15893  geoserg  15898  geolim  15902  geolim2  15903  georeclim  15904  geo2sum  15905  geoisum1c  15912  fallfacval2  16043  fallfacval3  16044  fallfaccl  16048  risefallfac  16056  fallfacp1  16062  0fallfac  16069  binomfallfaclem2  16072  bpoly2  16089  bpoly3  16090  fsumcube  16092  tanadd  16199  addsin  16202  fzocongeq  16357  odd2np1  16374  divalglem9  16434  phiprm  16810  pythagtriplem4  16852  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  fldivp1  16930  4sqlem19  16996  vdwapun  17007  vdwlem6  17019  xrsdsreclb  21448  cnmet  24807  icccvx  24994  reparphti  25042  reparphtiOLD  25043  pcorevlem  25072  cncmet  25369  dveflem  26031  dvef  26032  dv11cn  26054  coeeulem  26277  geolim3  26395  abelthlem2  26490  abelthlem7  26496  efimpi  26547  ptolemy  26552  tangtx  26561  abssinper  26577  cosne0  26585  tanregt0  26595  eflogeq  26658  logneg2  26671  advlogexp  26711  logtayl  26716  logtayl2  26718  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  lawcos  26873  pythag  26874  isosctrlem1  26875  isosctrlem2  26876  asinlem  26925  asinlem2  26926  asinlem3a  26927  asinlem3  26928  asinf  26929  acosf  26931  atanf  26937  asinneg  26943  efiasin  26945  sinasin  26946  asinsin  26949  acoscos  26950  asinbnd  26956  cosasin  26961  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  efiatan2  26974  2efiatan  26975  cosatan  26978  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  atantayl2  26995  birthdaylem2  27009  scvxcvx  27043  basellem8  27145  1sgm2ppw  27258  logfacbnd3  27281  logfacrlim  27282  perfect1  27286  dchrsum2  27326  sumdchr2  27328  bposlem9  27350  lgsquad2  27444  addsq2reu  27498  rplogsumlem1  27542  dchrmusum2  27552  log2sumbnd  27602  pntrsumo1  27623  brbtwn2  28934  colinearalg  28939  axcgrid  28945  axsegconlem1  28946  ax5seglem1  28957  ax5seglem2  28958  ax5seglem3  28960  ax5seglem5  28962  ax5seglem9  28966  axbtwnid  28968  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  crctcshwlkn0lem6  29844  eucrctshift  30271  hvmulcan2  31101  subfacp1lem6  35169  cvxsconn  35227  resconn  35230  sinccvglem  35656  sin2h  37596  tan2h  37598  itg2addnclem3  37659  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  dvasin  37690  dvacos  37691  lcmineqlem4  42013  lcmineqlem8  42017  rmspecsqrtnq  42893  jm2.17a  42948  acongeq  42971  jm2.27c  42995  lhe4.4ex1a  44324  dvconstbi  44329  abssubrp  45225  cnambpcma  47243