Theorem subcl 11474

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃!wreu 3370  ℩crio 7379  (class class class)co 7423  ℂcc 11116   + caddc 11121   − cmin 11459

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266  df-sub 11461

This theorem is used by:  negcl  11475  subf  11477  pncan3  11483  npcan  11484  addsubass  11485  addsub  11486  addsub12  11488  addsubeq4  11490  npncan  11497  nppcan  11498  nnpcan  11499  nppcan3  11500  subcan2  11501  subsub2  11504  subsub4  11509  nnncan  11511  nnncan1  11512  nnncan2  11513  npncan3  11514  addsub4  11519  subadd4  11520  peano2cnm  11542  subcli  11552  subcld  11587  subeqrev  11654  subdi  11665  subdir  11666  mulsub2  11676  recextlem1  11862  recex  11864  mulcan1g  11885  div2sub  12058  cju  12232  halfaddsubcl  12494  halfaddsub  12495  iccf1o  13541  modsumfzodifsn  14000  sersub  14101  sqsubswap  14173  subsq  14266  subsq2  14267  bcn2  14375  pfxccatin12lem1  14789  pfxccatin12lem2  14792  shftval2  15138  2shfti  15143  sqabssub  15360  abssub  15404  abs3dif  15409  abs2dif  15410  abs2difabs  15412  climuni  15629  cjcn2  15677  recn2  15678  imcn2  15679  o1sub  15693  climsub  15711  caucvgr  15753  iseralt  15762  fsum0diag2  15860  arisum2  15941  geoserg  15946  geolim  15950  geolim2  15951  georeclim  15952  geo2sum  15953  geoisum1c  15960  fallfacval2  16091  fallfacval3  16092  fallfaccl  16096  risefallfac  16104  fallfacp1  16109  0fallfac  16116  binomfallfaclem2  16119  bpoly2  16136  bpoly3  16137  fsumcube  16139  tanadd  16248  addsin  16251  fzocongeq  16407  odd2np1  16424  divalglem9  16484  phiprm  16861  pythagtriplem4  16904  pythagtriplem12  16911  pythagtriplem14  16913  pythagtriplem16  16915  fldivp1  16982  4sqlem19  17048  vdwapun  17059  vdwlem6  17071  xrsdsreclb  21601  cnmet  24965  icccvx  25146  reparphti  25193  pcorevlem  25222  cncmet  25518  dveflem  26175  dvef  26176  dv11cn  26197  coeeulem  26418  geolim3  26539  abelthlem2  26632  abelthlem7  26638  efimpi  26693  ptolemy  26698  tangtx  26707  abssinper  26723  cosne0  26731  tanregt0  26741  eflogeq  26804  logneg2  26817  advlogexp  26857  logtayl  26862  logtayl2  26864  ang180lem1  27011  ang180lem2  27012  ang180lem3  27013  lawcos  27018  pythag  27019  isosctrlem1  27020  isosctrlem2  27021  asinlem  27070  asinlem2  27071  asinlem3a  27072  asinlem3  27073  asinf  27074  acosf  27076  atanf  27082  asinneg  27088  efiasin  27090  sinasin  27091  asinsin  27094  acoscos  27095  asinbnd  27101  cosasin  27106  atanneg  27109  atancj  27112  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsublem  27117  atanlogsub  27118  efiatan2  27119  2efiatan  27120  cosatan  27123  atantan  27125  atanbndlem  27127  atans2  27133  dvatan  27137  atantayl  27139  atantayl2  27140  birthdaylem2  27154  scvxcvx  27187  basellem8  27289  1sgm2ppw  27401  logfacbnd3  27424  logfacrlim  27425  perfect1  27429  dchrsum2  27469  sumdchr2  27471  bposlem9  27493  lgsquad2  27587  addsq2reu  27641  rplogsumlem1  27685  dchrmusum2  27695  log2sumbnd  27745  pntrsumo1  27766  brbtwn2  29292  colinearalg  29297  axcgrid  29303  axsegconlem1  29304  ax5seglem1  29315  ax5seglem2  29316  ax5seglem3  29318  ax5seglem5  29320  ax5seglem9  29324  axbtwnid  29326  axeuclidlem  29349  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem8  29358  crctcshwlkn0lem6  30201  eucrctshift  30631  hvmulcan2  31462  subfacp1lem6  35697  cvxsconn  35755  resconn  35758  sinccvglem  36184  sin2h  38301  tan2h  38303  itg2addnclem3  38364  ftc1anclem4  38387  ftc1anclem5  38388  ftc1anclem6  38389  ftc1anclem7  38390  ftc1anc  38392  dvasin  38395  dvacos  38396  lcmineqlem4  42839  lcmineqlem8  42843  rmspecsqrtnq  43673  jm2.17a  43727  acongeq  43750  jm2.27c  43774  lhe4.4ex1a  45079  dvconstbi  45084  abssubrp  46035  cnambpcma  48071