Theorem subcl 11583

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 11575	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11574	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 464	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7417	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 18	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2864	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃!wreu 3367  ℩crio 7399  (class class class)co 7443  ℂcc 11225   + caddc 11230   − cmin 11568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375  df-sub 11570

This theorem is used by:  negcl  11584  subf  11586  pncan3  11592  npcan  11593  addsubass  11594  addsub  11595  addsub12  11597  addsubeq4  11599  npncan  11606  nppcan  11607  nnpcan  11608  nppcan3  11609  subcan2  11610  subsub2  11613  subsub4  11618  nnncan  11620  nnncan1  11621  nnncan2  11622  npncan3  11623  addsub4  11628  subadd4  11629  peano2cnm  11651  subcli  11661  subcld  11696  subeqrev  11765  subdi  11776  subdir  11777  mulsub2  11787  recextlem1  11973  recex  11975  mulcan1g  11996  div2sub  12169  cju  12343  halfaddsubcl  12605  halfaddsub  12606  iccf1o  13654  modsumfzodifsn  14114  sersub  14215  sqsubswap  14287  subsq  14381  subsq2  14382  bcn2  14490  pfxccatin12lem1  14905  pfxccatin12lem2  14908  shftval2  15257  2shfti  15262  sqabssub  15479  abssub  15523  abs3dif  15528  abs2dif  15529  abs2difabs  15531  climuni  15748  cjcn2  15796  recn2  15797  imcn2  15798  o1sub  15812  climsub  15830  caucvgr  15872  iseralt  15881  fsum0diag2  15978  geoserg  16064  geolim  16068  geolim2  16069  georeclim  16070  geo2sum  16071  geoisum1c  16078  fallfacval2  16207  fallfacval3  16208  fallfaccl  16212  risefallfac  16220  fallfacp1  16225  0fallfac  16232  binomfallfaclem2  16235  bpoly2  16252  bpoly3  16253  fsumcube  16255  tanadd  16364  addsin  16367  fzocongeq  16523  odd2np1  16540  divalglem9  16600  phiprm  16983  pythagtriplem4  17026  pythagtriplem12  17033  pythagtriplem14  17035  pythagtriplem16  17037  fldivp1  17104  4sqlem19  17170  vdwapun  17181  vdwlem6  17193  xrsdsreclb  21750  cnmet  25120  icccvx  25301  reparphti  25348  pcorevlem  25377  cncmet  25673  dveflem  26329  dvef  26330  dv11cn  26351  coeeulem  26573  geolim3  26696  abelthlem2  26789  abelthlem7  26795  efimpi  26850  ptolemy  26855  tangtx  26864  abssinper  26879  cosne0  26887  tanregt0  26897  eflogeq  26960  logneg2  26973  advlogexp  27013  logtayl  27018  logtayl2  27020  ang180lem1  27167  ang180lem2  27168  ang180lem3  27169  lawcos  27174  pythag  27175  isosctrlem1  27176  isosctrlem2  27177  asinlem  27226  asinlem2  27227  asinlem3a  27228  asinlem3  27229  asinf  27230  acosf  27232  atanf  27238  asinneg  27244  efiasin  27246  sinasin  27247  asinsin  27250  acoscos  27251  asinbnd  27257  cosasin  27262  atanneg  27265  atancj  27268  efiatan  27270  atanlogaddlem  27271  atanlogadd  27272  atanlogsublem  27273  atanlogsub  27274  efiatan2  27275  2efiatan  27276  cosatan  27279  atantan  27281  atanbndlem  27283  atans2  27289  dvatan  27293  atantayl  27295  atantayl2  27296  birthdaylem2  27310  scvxcvx  27343  basellem8  27445  1sgm2ppw  27557  logfacbnd3  27580  logfacrlim  27581  perfect1  27585  dchrsum2  27625  sumdchr2  27627  bposlem9  27649  lgsquad2  27743  addsq2reu  27797  rplogsumlem1  27841  dchrmusum2  27851  log2sumbnd  27901  pntrsumo1  27922  brbtwn2  29513  colinearalg  29518  axcgrid  29524  axsegconlem1  29525  ax5seglem1  29536  ax5seglem2  29537  ax5seglem3  29539  ax5seglem5  29541  ax5seglem9  29545  axbtwnid  29547  axeuclidlem  29570  axcontlem2  29573  axcontlem4  29575  axcontlem7  29578  axcontlem8  29579  crctcshwlkn0lem6  30434  eucrctshift  30874  hvmulcan2  31705  subfacp1lem6  36117  cvxsconn  36175  resconn  36178  sinccvglem  36604  sin2h  38725  tan2h  38727  itg2addnclem3  38783  ftc1anclem4  38806  ftc1anclem5  38807  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anc  38811  dvasin  38814  dvacos  38815  lcmineqlem4  43274  lcmineqlem8  43278  rmspecsqrtnq  44106  jm2.17a  44160  acongeq  44183  jm2.27c  44207  lhe4.4ex1a  45505  dvconstbi  45510  abssubrp  46497  cnambpcma  48569