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

Theorem difexg 4311
Description: Existence of a difference. (Contributed by NM, 26-May-1998.)
Assertion
Ref Expression
difexg  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )

Proof of Theorem difexg
StepHypRef Expression
1 difss 3434 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4309 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 652 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   _Vcvv 2916    \ cdif 3277    C_ wss 3280
This theorem is referenced by:  difex2  4673  elpwun  4715  2oconcl  6706  fnoe  6713  difsnen  7149  domdifsn  7150  domunsncan  7167  fodomr  7217  domss2  7225  domssex2  7226  domssex  7227  mapdom2  7237  limenpsi  7241  sucdom2  7262  findcard  7306  findcard2  7307  frfi  7311  unfilem3  7332  marypha1lem  7396  brwdom2  7497  infeq5i  7547  infdifsn  7567  dfac8clem  7869  acni  7882  dfac9  7972  dfacacn  7977  kmlem11  7996  kmlem12  7997  infpss  8053  ssfin4  8146  fin23lem28  8176  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  isf34lem1  8208  compssiso  8210  enfin1ai  8220  fin1a2lem7  8242  fin1a2lem13  8248  axdc2lem  8284  axcclem  8293  zornn0g  8341  fpwwe2lem13  8473  fpwwe2  8474  canthp1lem1  8483  grothprim  8665  hashbclem  11656  hashf1lem1  11659  brfi1uzind  11670  ramub1lem1  13349  mrieqv2d  13819  mreexexlemd  13824  pltfval  14371  isirred  15759  isdrng2  15800  drngmcl  15803  drngid2  15806  isdrngd  15815  lssset  15965  xrs1mnd  16691  xrs1cmn  16693  xrge0subm  16694  cnmsubglem  16716  basdif0  16973  tgdif0  17012  clsval2  17069  neitr  17198  lecldbas  17237  pnrmopn  17361  cmpcld  17419  cmpfi  17425  csdfil  17879  ufileu  17904  filufint  17905  alexsublem  18028  ptcmplem2  18037  xrge0gsumle  18817  xrge0tsms  18818  bcth3  19237  iunmbl  19400  i1fd  19526  tdeglem4  19936  reefgim  20319  usgrares1  21377  cusgrares  21434  cusgrafilem3  21443  ablomul  21896  eigvecval  23352  disjdifprg  23970  xrge00  24161  xrge0tsmsd  24176  esummono  24403  gsumesum  24404  insiga  24473  sitgclg  24609  ballotlemfrc  24737  ballotlem8  24747  subfacp1lem5  24823  iscvm  24899  cvmsval  24906  axlowdimlem15  25799  axlowdim  25804  voliunnfl  26149  fdc  26339  isdrngo2  26464  ralxpmap  26632  lzenom  26718  diophin  26721  diophren  26764  islindf4  27176  pmtrfv  27263  cntzsdrg  27378  deg1mhm  27394  stoweidlem57  27673  frgrawopreglem1  28147  bnj852  28998  bnj865  29000  watvalN  30475  hvmapfval  32242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator