Theorem subcl 10877

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108  ∃!wreu 3138  ℩crio 7105  (class class class)co 7148  ℂcc 10527   + caddc 10532   − cmin 10862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-sub 10864

This theorem is referenced by:  negcl  10878  subf  10880  pncan3  10886  npcan  10887  addsubass  10888  addsub  10889  addsub12  10891  addsubeq4  10893  npncan  10899  nppcan  10900  nnpcan  10901  nppcan3  10902  subcan2  10903  subsub2  10906  subsub4  10911  nnncan  10913  nnncan1  10914  nnncan2  10915  npncan3  10916  addsub4  10921  subadd4  10922  peano2cnm  10944  subcli  10954  subcld  10989  subeqrev  11054  subdi  11065  subdir  11066  mulsub2  11076  recextlem1  11262  recex  11264  mulcan1g  11285  div2sub  11457  cju  11626  halfaddsubcl  11861  halfaddsub  11862  iccf1o  12874  modsumfzodifsn  13304  sersub  13405  sqsubswap  13475  subsq  13564  subsq2  13565  bcn2  13671  pfxccatin12lem1  14082  pfxccatin12lem2  14085  shftval2  14426  2shfti  14431  sqabssub  14635  abssub  14678  abs3dif  14683  abs2dif  14684  abs2difabs  14686  climuni  14901  cjcn2  14948  recn2  14949  imcn2  14950  o1sub  14964  climsub  14982  caucvgr  15024  iseralt  15033  fsum0diag2  15130  arisum2  15208  geoserg  15213  geolim  15218  geolim2  15219  georeclim  15220  geo2sum  15221  geoisum1c  15228  fallfacval2  15357  fallfacval3  15358  fallfaccl  15362  risefallfac  15370  fallfacp1  15376  0fallfac  15383  binomfallfaclem2  15386  bpoly2  15403  bpoly3  15404  fsumcube  15406  tanadd  15512  addsin  15515  fzocongeq  15666  odd2np1  15682  divalglem9  15744  phiprm  16106  pythagtriplem4  16148  pythagtriplem12  16155  pythagtriplem14  16157  pythagtriplem16  16159  fldivp1  16225  4sqlem19  16291  vdwapun  16302  vdwlem6  16314  xrsdsreclb  20584  cnmet  23372  icccvx  23546  reparphti  23593  pcorevlem  23622  cncmet  23917  dveflem  24568  dvef  24569  dv11cn  24590  coeeulem  24806  geolim3  24920  abelthlem2  25012  abelthlem7  25018  efimpi  25069  ptolemy  25074  tangtx  25083  abssinper  25098  cosne0  25106  tanregt0  25115  eflogeq  25177  logneg2  25190  advlogexp  25230  logtayl  25235  logtayl2  25237  ang180lem1  25379  ang180lem2  25380  ang180lem3  25381  lawcos  25386  pythag  25387  isosctrlem1  25388  isosctrlem2  25389  asinlem  25438  asinlem2  25439  asinlem3a  25440  asinlem3  25441  asinf  25442  acosf  25444  atanf  25450  asinneg  25456  efiasin  25458  sinasin  25459  asinsin  25462  acoscos  25463  asinbnd  25469  cosasin  25474  atanneg  25477  atancj  25480  efiatan  25482  atanlogaddlem  25483  atanlogadd  25484  atanlogsublem  25485  atanlogsub  25486  efiatan2  25487  2efiatan  25488  cosatan  25491  atantan  25493  atanbndlem  25495  atans2  25501  dvatan  25505  atantayl  25507  atantayl2  25508  birthdaylem2  25522  scvxcvx  25555  basellem8  25657  1sgm2ppw  25768  logfacbnd3  25791  logfacrlim  25792  perfect1  25796  dchrsum2  25836  sumdchr2  25838  bposlem9  25860  lgsquad2  25954  addsq2reu  26008  rplogsumlem1  26052  dchrmusum2  26062  log2sumbnd  26112  pntrsumo1  26133  brbtwn2  26683  colinearalg  26688  axcgrid  26694  axsegconlem1  26695  ax5seglem1  26706  ax5seglem2  26707  ax5seglem3  26709  ax5seglem5  26711  ax5seglem9  26715  axbtwnid  26717  axeuclidlem  26740  axcontlem2  26743  axcontlem4  26745  axcontlem7  26748  axcontlem8  26749  crctcshwlkn0lem6  27585  eucrctshift  28014  hvmulcan2  28842  subfacp1lem6  32425  cvxsconn  32483  resconn  32486  sinccvglem  32908  sin2h  34874  tan2h  34876  itg2addnclem3  34937  ftc1anclem4  34962  ftc1anclem5  34963  ftc1anclem6  34964  ftc1anclem7  34965  ftc1anc  34967  dvasin  34970  dvacos  34971  rmspecsqrtnq  39494  jm2.17a  39548  acongeq  39571  jm2.27c  39595  lhe4.4ex1a  40652  dvconstbi  40657  abssubrp  41531  cnambpcma  43485