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

Theorem difexg 4582
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 3614 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4580 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 670 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   _Vcvv 3093    \ cdif 3456    C_ wss 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-dif 3462  df-in 3466  df-ss 3473
This theorem is referenced by:  difex2  6589  elpwun  6595  2oconcl  7152  fnoe  7159  ralxpmap  7467  difsnen  7598  domdifsn  7599  domunsncan  7616  fodomr  7667  domss2  7675  domssex2  7676  domssex  7677  mapdom2  7687  limenpsi  7691  sucdom2  7713  findcard  7758  findcard2  7759  frfi  7764  unfilem3  7785  marypha1lem  7892  brwdom2  7999  infeq5i  8053  infdifsn  8073  dfac8clem  8413  acni  8426  dfac9  8516  dfacacn  8521  kmlem11  8540  kmlem12  8541  infpss  8597  ssfin4  8690  fin23lem28  8720  isf32lem6  8738  isf32lem7  8739  isf32lem8  8740  isf34lem1  8752  compssiso  8754  enfin1ai  8764  fin1a2lem7  8786  fin1a2lem13  8792  axdc2lem  8828  axcclem  8837  zornn0g  8885  fpwwe2lem13  9020  fpwwe2  9021  canthp1lem1  9030  grothprim  9212  hashbclem  12477  hashf1lem1  12480  brfi1uzind  12508  ramub1lem1  14418  mrieqv2d  14910  mreexexlemd  14915  pltfval  15460  pmtrfv  16348  dpjidcl  16978  isirred  17219  isdrng2  17277  drngmcl  17280  drngid2  17283  isdrngd  17292  lssset  17451  xrs1mnd  18327  xrs1cmn  18329  xrge0subm  18330  cnmsubglem  18351  islindf4  18743  smadiadetlem1a  19035  basdif0  19324  tgdif0  19364  clsval2  19421  neitr  19551  lecldbas  19590  pnrmopn  19714  cmpcld  19772  cmpfi  19778  csdfil  20265  ufileu  20290  filufint  20291  alexsublem  20414  ptcmplem2  20423  xrge0gsumle  21208  xrge0tsms  21209  bcth3  21640  iunmbl  21833  i1fd  21958  tdeglem4  22328  reefgim  22714  axlowdimlem15  24128  axlowdim  24133  elntg  24156  usgrares1  24279  cusgrares  24341  cusgrafilem3  24350  nbhashuvtx1  24784  frgrawopreglem1  24913  ablomul  25226  eigvecval  26684  disjdifprg  27305  resf1o  27422  xrge00  27544  xrge0tsmsd  27645  locfinref  27714  esummono  27936  insiga  28007  sitgclg  28154  ballotlemfrc  28335  ballotlem8  28345  subfacp1lem5  28498  iscvm  28574  cvmsval  28581  mdvval  28734  voliunnfl  30030  fdc  30210  isdrngo2  30333  lzenom  30675  diophin  30678  diophren  30719  cntzsdrg  31124  deg1mhm  31140  stoweidlem57  31728  fourierdlem102  31880  fourierdlem114  31892  usgresvm1  32281  usgresvm1ALT  32285  lincdifsn  32755  lindslinindsimp1  32788  lindslinindimp2lem2  32790  lindslinindimp2lem4  32792  lindslinindsimp2lem5  32793  lindslinindsimp2  32794  lincresunit1  32808  lincresunit2  32809  lincresunit3lem2  32811  lincresunit3  32812  bnj852  33707  bnj865  33709  watvalN  35440  hvmapfval  37209  ssdifcl  37442  sssymdifcl  37443
  Copyright terms: Public domain W3C validator