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

Theorem difexg 4595
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 3631 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4593 . 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 1767   _Vcvv 3113    \ cdif 3473    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490
This theorem is referenced by:  difex2  6585  elpwun  6591  2oconcl  7150  fnoe  7157  ralxpmap  7465  difsnen  7596  domdifsn  7597  domunsncan  7614  fodomr  7665  domss2  7673  domssex2  7674  domssex  7675  mapdom2  7685  limenpsi  7689  sucdom2  7711  findcard  7755  findcard2  7756  frfi  7761  unfilem3  7782  marypha1lem  7889  brwdom2  7995  infeq5i  8049  infdifsn  8069  dfac8clem  8409  acni  8422  dfac9  8512  dfacacn  8517  kmlem11  8536  kmlem12  8537  infpss  8593  ssfin4  8686  fin23lem28  8716  isf32lem6  8734  isf32lem7  8735  isf32lem8  8736  isf34lem1  8748  compssiso  8750  enfin1ai  8760  fin1a2lem7  8782  fin1a2lem13  8788  axdc2lem  8824  axcclem  8833  zornn0g  8881  fpwwe2lem13  9016  fpwwe2  9017  canthp1lem1  9026  grothprim  9208  hashbclem  12463  hashf1lem1  12466  brfi1uzind  12494  ramub1lem1  14399  mrieqv2d  14890  mreexexlemd  14895  pltfval  15442  pmtrfv  16273  dpjidcl  16897  isirred  17132  isdrng2  17189  drngmcl  17192  drngid2  17195  isdrngd  17204  lssset  17363  xrs1mnd  18224  xrs1cmn  18226  xrge0subm  18227  cnmsubglem  18248  islindf4  18640  smadiadetlem1a  18932  basdif0  19221  tgdif0  19260  clsval2  19317  neitr  19447  lecldbas  19486  pnrmopn  19610  cmpcld  19668  cmpfi  19674  csdfil  20130  ufileu  20155  filufint  20156  alexsublem  20279  ptcmplem2  20288  xrge0gsumle  21073  xrge0tsms  21074  bcth3  21505  iunmbl  21698  i1fd  21823  tdeglem4  22193  reefgim  22579  axlowdimlem15  23935  axlowdim  23940  elntg  23963  usgrares1  24086  cusgrares  24148  cusgrafilem3  24157  nbhashuvtx1  24591  frgrawopreglem1  24721  ablomul  25033  eigvecval  26491  disjdifprg  27109  resf1o  27225  xrge00  27336  xrge0tsmsd  27438  esummono  27706  insiga  27777  sitgclg  27924  ballotlemfrc  28105  ballotlem8  28115  subfacp1lem5  28268  iscvm  28344  cvmsval  28351  voliunnfl  29635  fdc  29841  isdrngo2  29964  lzenom  30307  diophin  30310  diophren  30351  cntzsdrg  30756  deg1mhm  30772  stoweidlem57  31357  fourierdlem102  31509  fourierdlem114  31521  usgresvm1  31912  usgresvm1ALT  31916  lincdifsn  32098  lindslinindsimp1  32131  lindslinindimp2lem2  32133  lindslinindimp2lem4  32135  lindslinindsimp2lem5  32136  lindslinindsimp2  32137  lincresunit1  32151  lincresunit2  32152  lincresunit3lem2  32154  lincresunit3  32155  bnj852  33058  bnj865  33060  watvalN  34789  hvmapfval  36556  ssdifcl  36776  sssymdifcl  36777
  Copyright terms: Public domain W3C validator