Theorem subcl 10280

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 10272	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 10271	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 469	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 6625	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2701	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∃!wreu 2914  ℩crio 6610  (class class class)co 6650  ℂcc 9934   + caddc 9939   − cmin 10266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079  df-sub 10268

This theorem is referenced by:  negcl  10281  subf  10283  pncan3  10289  npcan  10290  addsubass  10291  addsub  10292  addsub12  10294  addsubeq4  10296  npncan  10302  nppcan  10303  nnpcan  10304  nppcan3  10305  subcan2  10306  subsub2  10309  subsub4  10314  nnncan  10316  nnncan1  10317  nnncan2  10318  npncan3  10319  addsub4  10324  subadd4  10325  peano2cnm  10347  subcli  10357  subcld  10392  subeqrev  10453  subdi  10463  subdir  10464  mulsub2  10474  recextlem1  10657  recex  10659  mulcan1g  10680  div2sub  10850  cju  11016  halfaddsubcl  11264  halfaddsub  11265  iccf1o  12316  modsumfzodifsn  12743  sersub  12844  sqsubswap  12924  subsq  12972  subsq2  12973  bcn2  13106  swrdccatin12lem2b  13486  swrdccatin12lem2  13489  shftval2  13815  2shfti  13820  sqabssub  14023  abssub  14066  abs3dif  14071  abs2dif  14072  abs2difabs  14074  climuni  14283  cjcn2  14330  recn2  14331  imcn2  14332  o1sub  14346  climsub  14364  caucvgr  14406  iseralt  14415  fsum0diag2  14515  arisum2  14593  geoserg  14598  geolim  14601  geolim2  14602  georeclim  14603  geo2sum  14604  geoisum1c  14611  fallfacval2  14742  fallfacval3  14743  fallfaccl  14747  risefallfac  14755  fallfacp1  14761  0fallfac  14768  binomfallfaclem2  14771  bpoly2  14788  bpoly3  14789  fsumcube  14791  tanadd  14897  addsin  14900  fzocongeq  15046  odd2np1  15065  divalglem9  15124  phiprm  15482  pythagtriplem4  15524  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  fldivp1  15601  4sqlem19  15667  vdwapun  15678  vdwlem6  15690  xrsdsreclb  19793  cnmet  22575  icccvx  22749  reparphti  22797  pcorevlem  22826  cncmet  23119  dveflem  23742  dvef  23743  dv11cn  23764  coeeulem  23980  geolim3  24094  abelthlem2  24186  abelthlem7  24192  efimpi  24243  ptolemy  24248  tangtx  24257  abssinper  24270  cosne0  24276  tanregt0  24285  eflogeq  24348  logneg2  24361  advlogexp  24401  logtayl  24406  logtayl2  24408  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  lawcos  24546  pythag  24547  isosctrlem1  24548  isosctrlem2  24549  asinlem  24595  asinlem2  24596  asinlem3a  24597  asinlem3  24598  asinf  24599  acosf  24601  atanf  24607  asinneg  24613  efiasin  24615  sinasin  24616  asinsin  24619  acoscos  24620  asinbnd  24626  cosasin  24631  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  cosatan  24648  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  birthdaylem2  24679  scvxcvx  24712  basellem8  24814  1sgm2ppw  24925  logfacbnd3  24948  logfacrlim  24949  perfect1  24953  dchrsum2  24993  sumdchr2  24995  bposlem9  25017  lgsquad2  25111  rplogsumlem1  25173  dchrmusum2  25183  log2sumbnd  25233  pntrsumo1  25254  brbtwn2  25785  colinearalg  25790  axcgrid  25796  axsegconlem1  25797  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem9  25817  axbtwnid  25819  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  crctcshwlkn0lem6  26707  eucrctshift  27103  hvmulcan2  27930  subfacp1lem6  31167  cvxsconn  31225  resconn  31228  sinccvglem  31566  sin2h  33399  tan2h  33401  itg2addnclem3  33463  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493  dvasin  33496  dvacos  33497  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  jm2.17a  37527  acongeq  37550  jm2.27c  37574  lhe4.4ex1a  38528  dvconstbi  38533  abssubrp  39487  cnambpcma  41309  pfxccatin12lem1  41423  pfxccatin12lem2  41424