MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difexg Unicode version

Theorem difexg 4600
Description: Existence of a difference. (Contributed by NM, 26-May-1998.)
Assertion
Ref Expression
difexg

Proof of Theorem difexg
StepHypRef Expression
1 difss 3630 . 2
2 ssexg 4598 . 2
31, 2mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cvv 3109  \cdif 3472  C_wss 3475
This theorem is referenced by:  difex2  6607  elpwun  6613  2oconcl  7172  fnoe  7179  ralxpmap  7488  difsnen  7619  domdifsn  7620  domunsncan  7637  fodomr  7688  domss2  7696  domssex2  7697  domssex  7698  mapdom2  7708  limenpsi  7712  sucdom2  7734  findcard  7779  findcard2  7780  frfi  7785  unfilem3  7806  marypha1lem  7913  brwdom2  8020  infeq5i  8074  infdifsn  8094  dfac8clem  8434  acni  8447  dfac9  8537  dfacacn  8542  kmlem11  8561  kmlem12  8562  infpss  8618  ssfin4  8711  fin23lem28  8741  isf32lem6  8759  isf32lem7  8760  isf32lem8  8761  isf34lem1  8773  compssiso  8775  enfin1ai  8785  fin1a2lem7  8807  fin1a2lem13  8813  axdc2lem  8849  axcclem  8858  zornn0g  8906  fpwwe2lem13  9041  fpwwe2  9042  canthp1lem1  9051  grothprim  9233  hashbclem  12501  hashf1lem1  12504  brfi1uzind  12532  ramub1lem1  14544  mrieqv2d  15036  mreexexlemd  15041  pltfval  15589  pmtrfv  16477  dpjidcl  17107  isirred  17348  isdrng2  17406  drngmcl  17409  drngid2  17412  isdrngd  17421  lssset  17580  xrs1mnd  18456  xrs1cmn  18458  xrge0subm  18459  cnmsubglem  18480  islindf4  18873  smadiadetlem1a  19165  basdif0  19454  tgdif0  19494  clsval2  19551  neitr  19681  lecldbas  19720  pnrmopn  19844  cmpcld  19902  cmpfi  19908  csdfil  20395  ufileu  20420  filufint  20421  alexsublem  20544  ptcmplem2  20553  xrge0gsumle  21338  xrge0tsms  21339  bcth3  21770  iunmbl  21963  i1fd  22088  tdeglem4  22458  reefgim  22845  axlowdimlem15  24259  axlowdim  24264  elntg  24287  usgrares1  24410  cusgrares  24472  cusgrafilem3  24481  nbhashuvtx1  24915  frgrawopreglem1  25044  ablomul  25357  eigvecval  26815  disjdifprg  27436  resf1o  27553  xrge00  27674  xrge0tsmsd  27775  locfinref  27844  esummono  28066  insiga  28137  sitgclg  28284  ballotlemfrc  28465  ballotlem8  28475  subfacp1lem5  28628  iscvm  28704  cvmsval  28711  mdvval  28864  voliunnfl  30058  fdc  30238  isdrngo2  30361  lzenom  30703  diophin  30706  diophren  30747  cntzsdrg  31151  deg1mhm  31167  stoweidlem57  31839  fourierdlem102  31991  fourierdlem114  32003  usgresvm1  32443  usgresvm1ALT  32447  lincdifsn  33025  lindslinindsimp1  33058  lindslinindimp2lem2  33060  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lincresunit1  33078  lincresunit2  33079  lincresunit3lem2  33081  lincresunit3  33082  bnj852  33979  bnj865  33981  watvalN  35717  hvmapfval  37486  ssdifcl  37756  sssymdifcl  37757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator