Theorem subcl 8150

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 8143	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
2		negeu 8142	. . . 4 |- ( ( B e. CC /\ A e. CC ) -> E! x e. CC ( B + x ) = A )
3	2	ancoms 268	. . 3 |- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( B + x ) = A )
4		riotacl 5840	. . 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 2254	1 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148   E!wreu 2457   iota_crio 5825  (class class class)co 5870   CCcc 7804   + caddc 7809   - cmin 8122

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-setind 4534  ax-resscn 7898  ax-1cn 7899  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-addcom 7906  ax-addass 7908  ax-distr 7910  ax-i2m1 7911  ax-0id 7914  ax-rnegex 7915  ax-cnre 7917

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-opab 4063  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-sub 8124

This theorem is referenced by:  negcl  8151  subf  8153  pncan3  8159  npcan  8160  addsubass  8161  addsub  8162  addsub12  8164  addsubeq4  8166  npncan  8172  nppcan  8173  nnpcan  8174  nppcan3  8175  subcan2  8176  subsub2  8179  subsub4  8184  nnncan  8186  nnncan1  8187  nnncan2  8188  npncan3  8189  addsub4  8194  subadd4  8195  peano2cnm  8217  subcli  8227  subcld  8262  subeqrev  8327  subdi  8336  subdir  8337  mulsub2  8353  recextlem1  8602  recexap  8604  div2subap  8788  cju  8912  halfaddsubcl  9146  halfaddsub  9147  iccf1o  9998  ser3sub  10499  sqsubswap  10573  subsq  10619  subsq2  10620  bcn2  10735  shftval2  10826  2shfti  10831  sqabssub  11056  abssub  11101  abs3dif  11105  abs2dif  11106  abs2difabs  11108  climuni  11292  cjcn2  11315  recn2  11316  imcn2  11317  climsub  11327  fisum0diag2  11446  arisum2  11498  geosergap  11505  geolim  11510  geolim2  11511  georeclim  11512  geo2sum  11513  tanaddap  11738  addsin  11741  fzocongeq  11854  odd2np1  11868  phiprm  12213  pythagtriplem4  12258  pythagtriplem12  12265  pythagtriplem14  12267  fldivp1  12336  cnmet  13812  dveflem  13969  dvef  13970  efimpi  14022  ptolemy  14027  tangtx  14041  abssinper  14049