Theorem subcl 8118

Description: Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)

Assertion

Ref	Expression
subcl	|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )

Proof of Theorem subcl

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		subval 8111	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
2		negeu 8110	. . . 4 |- ( ( B e. CC /\ A e. CC ) -> E! x e. CC ( B + x ) = A )
3	2	ancoms 266	. . 3 |- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( B + x ) = A )
4		riotacl 5823	. . 3 |- ( E! x e. CC ( B + x ) = A -> ( iota_ x e. CC ( B + x ) = A ) e. CC )
5	3, 4	syl 14	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( iota_ x e. CC ( B + x ) = A ) e. CC )
6	1, 5	eqeltrd 2247	1 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   e. wcel 2141   E!wreu 2450   iota_crio 5808  (class class class)co 5853   CCcc 7772   + caddc 7777   - cmin 8090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-setind 4521  ax-resscn 7866  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-iota 5160  df-fun 5200  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-sub 8092

This theorem is referenced by:  negcl  8119  subf  8121  pncan3  8127  npcan  8128  addsubass  8129  addsub  8130  addsub12  8132  addsubeq4  8134  npncan  8140  nppcan  8141  nnpcan  8142  nppcan3  8143  subcan2  8144  subsub2  8147  subsub4  8152  nnncan  8154  nnncan1  8155  nnncan2  8156  npncan3  8157  addsub4  8162  subadd4  8163  peano2cnm  8185  subcli  8195  subcld  8230  subeqrev  8295  subdi  8304  subdir  8305  mulsub2  8321  recextlem1  8569  recexap  8571  div2subap  8754  cju  8877  halfaddsubcl  9111  halfaddsub  9112  iccf1o  9961  ser3sub  10462  sqsubswap  10536  subsq  10582  subsq2  10583  bcn2  10698  shftval2  10790  2shfti  10795  sqabssub  11020  abssub  11065  abs3dif  11069  abs2dif  11070  abs2difabs  11072  climuni  11256  cjcn2  11279  recn2  11280  imcn2  11281  climsub  11291  fisum0diag2  11410  arisum2  11462  geosergap  11469  geolim  11474  geolim2  11475  georeclim  11476  geo2sum  11477  tanaddap  11702  addsin  11705  fzocongeq  11818  odd2np1  11832  phiprm  12177  pythagtriplem4  12222  pythagtriplem12  12229  pythagtriplem14  12231  fldivp1  12300  cnmet  13324  dveflem  13481  dvef  13482  efimpi  13534  ptolemy  13539  tangtx  13553  abssinper  13561