MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subcl Structured version   Visualization version   GIF version

Theorem subcl 10874
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.
StepHypRef Expression
1 subval 10866 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) = (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2 negeu 10865 . . . 4 ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
32ancoms 459 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4 riotacl 7120 . . 3 (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
53, 4syl 17 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
61, 5eqeltrd 2913 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  ∃!wreu 3140  crio 7102  (class class class)co 7145  cc 10524   + caddc 10529  cmin 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861
This theorem is referenced by:  negcl  10875  subf  10877  pncan3  10883  npcan  10884  addsubass  10885  addsub  10886  addsub12  10888  addsubeq4  10890  npncan  10896  nppcan  10897  nnpcan  10898  nppcan3  10899  subcan2  10900  subsub2  10903  subsub4  10908  nnncan  10910  nnncan1  10911  nnncan2  10912  npncan3  10913  addsub4  10918  subadd4  10919  peano2cnm  10941  subcli  10951  subcld  10986  subeqrev  11051  subdi  11062  subdir  11063  mulsub2  11073  recextlem1  11259  recex  11261  mulcan1g  11282  div2sub  11454  cju  11623  halfaddsubcl  11858  halfaddsub  11859  iccf1o  12872  modsumfzodifsn  13302  sersub  13403  sqsubswap  13473  subsq  13562  subsq2  13563  bcn2  13669  pfxccatin12lem1  14080  pfxccatin12lem2  14083  shftval2  14424  2shfti  14429  sqabssub  14633  abssub  14676  abs3dif  14681  abs2dif  14682  abs2difabs  14684  climuni  14899  cjcn2  14946  recn2  14947  imcn2  14948  o1sub  14962  climsub  14980  caucvgr  15022  iseralt  15031  fsum0diag2  15128  arisum2  15206  geoserg  15211  geolim  15216  geolim2  15217  georeclim  15218  geo2sum  15219  geoisum1c  15226  fallfacval2  15355  fallfacval3  15356  fallfaccl  15360  risefallfac  15368  fallfacp1  15374  0fallfac  15381  binomfallfaclem2  15384  bpoly2  15401  bpoly3  15402  fsumcube  15404  tanadd  15510  addsin  15513  fzocongeq  15664  odd2np1  15680  divalglem9  15742  phiprm  16104  pythagtriplem4  16146  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  fldivp1  16223  4sqlem19  16289  vdwapun  16300  vdwlem6  16312  xrsdsreclb  20522  cnmet  23309  icccvx  23483  reparphti  23530  pcorevlem  23559  cncmet  23854  dveflem  24505  dvef  24506  dv11cn  24527  coeeulem  24743  geolim3  24857  abelthlem2  24949  abelthlem7  24955  efimpi  25006  ptolemy  25011  tangtx  25020  abssinper  25035  cosne0  25041  tanregt0  25050  eflogeq  25112  logneg2  25125  advlogexp  25165  logtayl  25170  logtayl2  25172  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  lawcos  25321  pythag  25322  isosctrlem1  25323  isosctrlem2  25324  asinlem  25373  asinlem2  25374  asinlem3a  25375  asinlem3  25376  asinf  25377  acosf  25379  atanf  25385  asinneg  25391  efiasin  25393  sinasin  25394  asinsin  25397  acoscos  25398  asinbnd  25404  cosasin  25409  atanneg  25412  atancj  25415  efiatan  25417  atanlogaddlem  25418  atanlogadd  25419  atanlogsublem  25420  atanlogsub  25421  efiatan2  25422  2efiatan  25423  cosatan  25426  atantan  25428  atanbndlem  25430  atans2  25436  dvatan  25440  atantayl  25442  atantayl2  25443  birthdaylem2  25458  scvxcvx  25491  basellem8  25593  1sgm2ppw  25704  logfacbnd3  25727  logfacrlim  25728  perfect1  25732  dchrsum2  25772  sumdchr2  25774  bposlem9  25796  lgsquad2  25890  addsq2reu  25944  rplogsumlem1  25988  dchrmusum2  25998  log2sumbnd  26048  pntrsumo1  26069  brbtwn2  26619  colinearalg  26624  axcgrid  26630  axsegconlem1  26631  ax5seglem1  26642  ax5seglem2  26643  ax5seglem3  26645  ax5seglem5  26647  ax5seglem9  26651  axbtwnid  26653  axeuclidlem  26676  axcontlem2  26679  axcontlem4  26681  axcontlem7  26684  axcontlem8  26685  crctcshwlkn0lem6  27521  eucrctshift  27950  hvmulcan2  28778  subfacp1lem6  32330  cvxsconn  32388  resconn  32391  sinccvglem  32813  sin2h  34764  tan2h  34766  itg2addnclem3  34827  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anc  34857  dvasin  34860  dvacos  34861  rmspecsqrtnq  39383  jm2.17a  39437  acongeq  39460  jm2.27c  39484  lhe4.4ex1a  40541  dvconstbi  40546  abssubrp  41421  cnambpcma  43375
  Copyright terms: Public domain W3C validator