Theorem subcl 7625

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 7618	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2		negeu 7617	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
3	2	ancoms 264	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4		riotacl 5583	. . 3 ⊢ (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
5	3, 4	syl 14	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
6	1, 5	eqeltrd 2161	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1287   ∈ wcel 1436  ∃!wreu 2357  ℩crio 5568  (class class class)co 5613  ℂcc 7292   + caddc 7297   − cmin 7597

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010  ax-setind 4326  ax-resscn 7381  ax-1cn 7382  ax-icn 7384  ax-addcl 7385  ax-addrcl 7386  ax-mulcl 7387  ax-addcom 7389  ax-addass 7391  ax-distr 7393  ax-i2m1 7394  ax-0id 7397  ax-rnegex 7398  ax-cnre 7400

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-opab 3875  df-id 4094  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-iota 4946  df-fun 4983  df-fv 4989  df-riota 5569  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-sub 7599

This theorem is referenced by:  negcl  7626  subf  7628  pncan3  7634  npcan  7635  addsubass  7636  addsub  7637  addsub12  7639  addsubeq4  7641  npncan  7647  nppcan  7648  nnpcan  7649  nppcan3  7650  subcan2  7651  subsub2  7654  subsub4  7659  nnncan  7661  nnncan1  7662  nnncan2  7663  npncan3  7664  addsub4  7669  subadd4  7670  peano2cnm  7692  subcli  7702  subcld  7737  subeqrev  7798  subdi  7807  subdir  7808  mulsub2  7824  recextlem1  8059  recexap  8061  cju  8356  halfaddsubcl  8582  halfaddsub  8583  iccf1o  9353  isersub  9839  sqsubswap  9913  subsq  9958  subsq2  9959  bcn2  10068  shftval2  10156  2shfti  10161  sqabssub  10384  abssub  10429  abs3dif  10433  abs2dif  10434  abs2difabs  10436  climuni  10574  cjcn2  10596  recn2  10597  imcn2  10598  climsub  10608  fzocongeq  10734  odd2np1  10748  phiprm  11074