Theorem subcl 8519

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 8512	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 8511	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 268	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 6048	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 14	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2315	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  ∃!wreu 2530  ℩crio 6031  (class class class)co 6079  ℂcc 8171   + caddc 8176   − cmin 8491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-setind 4682  ax-resscn 8265  ax-1cn 8266  ax-icn 8268  ax-addcl 8269  ax-addrcl 8270  ax-mulcl 8271  ax-addcom 8273  ax-addass 8275  ax-distr 8277  ax-i2m1 8278  ax-0id 8281  ax-rnegex 8282  ax-cnre 8284

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-iota 5335  df-fun 5377  df-fv 5383  df-riota 6032  df-ov 6082  df-oprab 6083  df-mpo 6084  df-sub 8493

This theorem is referenced by:  negcl  8520  subf  8522  pncan3  8528  npcan  8529  addsubass  8530  addsub  8531  addsub12  8533  addsubeq4  8535  npncan  8541  nppcan  8542  nnpcan  8543  nppcan3  8544  subcan2  8545  subsub2  8548  subsub4  8553  nnncan  8555  nnncan1  8556  nnncan2  8557  npncan3  8558  addsub4  8563  subadd4  8564  peano2cnm  8586  subcli  8596  subcld  8631  subeqrev  8696  subdi  8706  subdir  8707  mulsub2  8723  recextlem1  8973  recexap  8975  div2subap  9161  cju  9285  ofnegsub  9286  halfaddsubcl  9521  halfaddsub  9522  iccf1o  10390  ser3sub  10943  sqsubswap  11019  subsq  11066  subsq2  11067  bcn2  11185  pfxccatin12lem1  11483  pfxccatin12lem2  11486  shftval2  11574  2shfti  11579  sqabssub  11805  abssub  11850  abs3dif  11854  abs2dif  11855  abs2difabs  11857  climuni  12042  cjcn2  12065  recn2  12066  imcn2  12067  climsub  12077  fisum0diag2  12197  arisum2  12249  geosergap  12256  geolim  12261  geolim2  12262  georeclim  12263  geo2sum  12264  tanaddap  12489  addsin  12492  fzocongeq  12608  odd2np1  12623  phiprm  12984  pythagtriplem4  13030  pythagtriplem12  13037  pythagtriplem14  13039  fldivp1  13110  4sqlem19  13171  cnmet  15614  dveflem  15810  dvef  15811  efimpi  15903  ptolemy  15908  tangtx  15922  abssinper  15930  birthdaylem2  16071  1sgm2ppw  16092  perfect1  16095  lgsquad2  16185