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

Theorem difexg 4199
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 3337 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4197 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 651 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   _Vcvv 2822    \ cdif 3183    C_ wss 3186
This theorem is referenced by:  difex2  4562  elpwun  4604  2oconcl  6544  fnoe  6551  difsnen  6987  domdifsn  6988  domunsncan  7005  fodomr  7055  domss2  7063  domssex2  7064  domssex  7065  mapdom2  7075  limenpsi  7079  sucdom2  7100  findcard  7142  findcard2  7143  frfi  7147  unfilem3  7168  marypha1lem  7231  brwdom2  7332  infeq5i  7382  infdifsn  7402  dfac8clem  7704  acni  7717  dfac9  7807  dfacacn  7812  kmlem11  7831  kmlem12  7832  infpss  7888  ssfin4  7981  fin23lem28  8011  isf32lem6  8029  isf32lem7  8030  isf32lem8  8031  isf34lem1  8043  compssiso  8045  enfin1ai  8055  fin1a2lem7  8077  fin1a2lem13  8083  axdc2lem  8119  axcclem  8128  zornn0g  8177  fpwwe2lem13  8309  fpwwe2  8310  canthp1lem1  8319  grothprim  8501  hashbclem  11437  hashf1lem1  11440  ramub1lem1  13120  mrieqv2d  13590  mreexexlemd  13595  pltfval  14142  isirred  15530  isdrng2  15571  drngmcl  15574  drngid2  15577  isdrngd  15586  lssset  15740  xrs1mnd  16465  xrs1cmn  16467  xrge0subm  16468  cnmsubglem  16490  basdif0  16747  tgdif0  16786  clsval2  16843  lecldbas  17005  pnrmopn  17127  cmpcld  17185  cmpfi  17191  csdfil  17641  ufileu  17666  filufint  17667  alexsublem  17790  ptcmplem2  17799  xrge0gsumle  18390  xrge0tsms  18391  bcth3  18806  iunmbl  18963  i1fd  19089  tdeglem4  19499  reefgim  19879  ablomul  21075  eigvecval  22531  disjdifprg  23160  xrge00  23346  xrge0tsmsd  23360  esummono  23626  gsumesum  23627  pwsiga  23689  insiga  23696  ballotlemfrc  23958  ballotlem8  23968  subfacp1lem5  23999  iscvm  24074  cvmsval  24081  axlowdimlem15  24970  axlowdim  24975  fdc  25604  isdrngo2  25737  ralxpmap  25909  lzenom  25997  diophin  26000  diophren  26044  islindf4  26456  pmtrfv  26543  cntzsdrg  26658  deg1mhm  26674  stoweidlem57  26954  bnj852  28464  bnj865  28466  watvalN  30000  hvmapfval  31767
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-dif 3189  df-in 3193  df-ss 3200
  Copyright terms: Public domain W3C validator