Theorem subcl 10885

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 10877	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 10876	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 461	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 7131	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2913	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃!wreu 3140  ℩crio 7113  (class class class)co 7156  ℂcc 10535   + caddc 10540   − cmin 10870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872

This theorem is referenced by:  negcl  10886  subf  10888  pncan3  10894  npcan  10895  addsubass  10896  addsub  10897  addsub12  10899  addsubeq4  10901  npncan  10907  nppcan  10908  nnpcan  10909  nppcan3  10910  subcan2  10911  subsub2  10914  subsub4  10919  nnncan  10921  nnncan1  10922  nnncan2  10923  npncan3  10924  addsub4  10929  subadd4  10930  peano2cnm  10952  subcli  10962  subcld  10997  subeqrev  11062  subdi  11073  subdir  11074  mulsub2  11084  recextlem1  11270  recex  11272  mulcan1g  11293  div2sub  11465  cju  11634  halfaddsubcl  11870  halfaddsub  11871  iccf1o  12883  modsumfzodifsn  13313  sersub  13414  sqsubswap  13484  subsq  13573  subsq2  13574  bcn2  13680  pfxccatin12lem1  14090  pfxccatin12lem2  14093  shftval2  14434  2shfti  14439  sqabssub  14643  abssub  14686  abs3dif  14691  abs2dif  14692  abs2difabs  14694  climuni  14909  cjcn2  14956  recn2  14957  imcn2  14958  o1sub  14972  climsub  14990  caucvgr  15032  iseralt  15041  fsum0diag2  15138  arisum2  15216  geoserg  15221  geolim  15226  geolim2  15227  georeclim  15228  geo2sum  15229  geoisum1c  15236  fallfacval2  15365  fallfacval3  15366  fallfaccl  15370  risefallfac  15378  fallfacp1  15384  0fallfac  15391  binomfallfaclem2  15394  bpoly2  15411  bpoly3  15412  fsumcube  15414  tanadd  15520  addsin  15523  fzocongeq  15674  odd2np1  15690  divalglem9  15752  phiprm  16114  pythagtriplem4  16156  pythagtriplem12  16163  pythagtriplem14  16165  pythagtriplem16  16167  fldivp1  16233  4sqlem19  16299  vdwapun  16310  vdwlem6  16322  xrsdsreclb  20592  cnmet  23380  icccvx  23554  reparphti  23601  pcorevlem  23630  cncmet  23925  dveflem  24576  dvef  24577  dv11cn  24598  coeeulem  24814  geolim3  24928  abelthlem2  25020  abelthlem7  25026  efimpi  25077  ptolemy  25082  tangtx  25091  abssinper  25106  cosne0  25114  tanregt0  25123  eflogeq  25185  logneg2  25198  advlogexp  25238  logtayl  25243  logtayl2  25245  ang180lem1  25387  ang180lem2  25388  ang180lem3  25389  lawcos  25394  pythag  25395  isosctrlem1  25396  isosctrlem2  25397  asinlem  25446  asinlem2  25447  asinlem3a  25448  asinlem3  25449  asinf  25450  acosf  25452  atanf  25458  asinneg  25464  efiasin  25466  sinasin  25467  asinsin  25470  acoscos  25471  asinbnd  25477  cosasin  25482  atanneg  25485  atancj  25488  efiatan  25490  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atanlogsub  25494  efiatan2  25495  2efiatan  25496  cosatan  25499  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  birthdaylem2  25530  scvxcvx  25563  basellem8  25665  1sgm2ppw  25776  logfacbnd3  25799  logfacrlim  25800  perfect1  25804  dchrsum2  25844  sumdchr2  25846  bposlem9  25868  lgsquad2  25962  addsq2reu  26016  rplogsumlem1  26060  dchrmusum2  26070  log2sumbnd  26120  pntrsumo1  26141  brbtwn2  26691  colinearalg  26696  axcgrid  26702  axsegconlem1  26703  ax5seglem1  26714  ax5seglem2  26715  ax5seglem3  26717  ax5seglem5  26719  ax5seglem9  26723  axbtwnid  26725  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  crctcshwlkn0lem6  27593  eucrctshift  28022  hvmulcan2  28850  subfacp1lem6  32432  cvxsconn  32490  resconn  32493  sinccvglem  32915  sin2h  34897  tan2h  34899  itg2addnclem3  34960  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anc  34990  dvasin  34993  dvacos  34994  rmspecsqrtnq  39523  jm2.17a  39577  acongeq  39600  jm2.27c  39624  lhe4.4ex1a  40681  dvconstbi  40686  abssubrp  41561  cnambpcma  43514