Theorem subcl 11457

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 11449	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 11448	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 463	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7386	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 18	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2863	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃!wreu 3367  ℩crio 7368  (class class class)co 7412  ℂcc 11099   + caddc 11104   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11444

This theorem is referenced by:  negcl  11458  subf  11460  pncan3  11466  npcan  11467  addsubass  11468  addsub  11469  addsub12  11471  addsubeq4  11473  npncan  11480  nppcan  11481  nnpcan  11482  nppcan3  11483  subcan2  11484  subsub2  11487  subsub4  11492  nnncan  11494  nnncan1  11495  nnncan2  11496  npncan3  11497  addsub4  11502  subadd4  11503  peano2cnm  11525  subcli  11535  subcld  11570  subeqrev  11637  subdi  11648  subdir  11649  mulsub2  11659  recextlem1  11845  recex  11847  mulcan1g  11868  div2sub  12041  cju  12215  halfaddsubcl  12477  halfaddsub  12478  iccf1o  13524  modsumfzodifsn  13982  sersub  14083  sqsubswap  14155  subsq  14248  subsq2  14249  bcn2  14357  pfxccatin12lem1  14767  pfxccatin12lem2  14770  shftval2  15114  2shfti  15119  sqabssub  15336  abssub  15380  abs3dif  15385  abs2dif  15386  abs2difabs  15388  climuni  15605  cjcn2  15653  recn2  15654  imcn2  15655  o1sub  15669  climsub  15687  caucvgr  15729  iseralt  15738  fsum0diag2  15836  arisum2  15917  geoserg  15922  geolim  15926  geolim2  15927  georeclim  15928  geo2sum  15929  geoisum1c  15936  fallfacval2  16067  fallfacval3  16068  fallfaccl  16072  risefallfac  16080  fallfacp1  16085  0fallfac  16092  binomfallfaclem2  16095  bpoly2  16112  bpoly3  16113  fsumcube  16115  tanadd  16224  addsin  16227  fzocongeq  16383  odd2np1  16400  divalglem9  16460  phiprm  16837  pythagtriplem4  16880  pythagtriplem12  16887  pythagtriplem14  16889  pythagtriplem16  16891  fldivp1  16958  4sqlem19  17024  vdwapun  17035  vdwlem6  17047  xrsdsreclb  21545  cnmet  24909  icccvx  25090  reparphti  25137  pcorevlem  25166  cncmet  25462  dveflem  26119  dvef  26120  dv11cn  26141  coeeulem  26362  geolim3  26481  abelthlem2  26573  abelthlem7  26579  efimpi  26634  ptolemy  26639  tangtx  26648  abssinper  26664  cosne0  26672  tanregt0  26682  eflogeq  26745  logneg2  26758  advlogexp  26798  logtayl  26803  logtayl2  26805  ang180lem1  26952  ang180lem2  26953  ang180lem3  26954  lawcos  26959  pythag  26960  isosctrlem1  26961  isosctrlem2  26962  asinlem  27011  asinlem2  27012  asinlem3a  27013  asinlem3  27014  asinf  27015  acosf  27017  atanf  27023  asinneg  27029  efiasin  27031  sinasin  27032  asinsin  27035  acoscos  27036  asinbnd  27042  cosasin  27047  atanneg  27050  atancj  27053  efiatan  27055  atanlogaddlem  27056  atanlogadd  27057  atanlogsublem  27058  atanlogsub  27059  efiatan2  27060  2efiatan  27061  cosatan  27064  atantan  27066  atanbndlem  27068  atans2  27074  dvatan  27078  atantayl  27080  atantayl2  27081  birthdaylem2  27095  scvxcvx  27128  basellem8  27230  1sgm2ppw  27342  logfacbnd3  27365  logfacrlim  27366  perfect1  27370  dchrsum2  27410  sumdchr2  27412  bposlem9  27434  lgsquad2  27528  addsq2reu  27582  rplogsumlem1  27626  dchrmusum2  27636  log2sumbnd  27686  pntrsumo1  27707  brbtwn2  29233  colinearalg  29238  axcgrid  29244  axsegconlem1  29245  ax5seglem1  29256  ax5seglem2  29257  ax5seglem3  29259  ax5seglem5  29261  ax5seglem9  29265  axbtwnid  29267  axeuclidlem  29290  axcontlem2  29293  axcontlem4  29295  axcontlem7  29298  axcontlem8  29299  crctcshwlkn0lem6  30142  eucrctshift  30572  hvmulcan2  31403  subfacp1lem6  35655  cvxsconn  35713  resconn  35716  sinccvglem  36142  sin2h  38239  tan2h  38241  itg2addnclem3  38302  ftc1anclem4  38325  ftc1anclem5  38326  ftc1anclem6  38327  ftc1anclem7  38328  ftc1anc  38330  dvasin  38333  dvacos  38334  lcmineqlem4  42777  lcmineqlem8  42781  rmspecsqrtnq  43613  jm2.17a  43667  acongeq  43690  jm2.27c  43714  lhe4.4ex1a  45019  dvconstbi  45024  abssubrp  45975  cnambpcma  48008