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

Theorem difexg 4542
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 3570 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4540 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 668 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   _Vcvv 3059    \ cdif 3411    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-dif 3417  df-in 3421  df-ss 3428
This theorem is referenced by:  difex2  6589  elpwun  6595  2oconcl  7190  fnoe  7197  ralxpmap  7506  difsnen  7637  domdifsn  7638  domunsncan  7655  fodomr  7706  domss2  7714  domssex2  7715  domssex  7716  mapdom2  7726  limenpsi  7730  sucdom2  7751  findcard  7793  findcard2  7794  frfi  7799  unfilem3  7820  marypha1lem  7927  brwdom2  8033  infeq5i  8086  infdifsn  8106  dfac8clem  8445  acni  8458  dfac9  8548  dfacacn  8553  kmlem11  8572  kmlem12  8573  infpss  8629  ssfin4  8722  fin23lem28  8752  isf32lem6  8770  isf32lem7  8771  isf32lem8  8772  isf34lem1  8784  compssiso  8786  enfin1ai  8796  fin1a2lem7  8818  fin1a2lem13  8824  axdc2lem  8860  axcclem  8869  zornn0g  8917  fpwwe2lem13  9050  fpwwe2  9051  canthp1lem1  9060  grothprim  9242  hashbclem  12550  hashf1lem1  12553  brfi1uzind  12581  ramub1lem1  14753  mrieqv2d  15253  mreexexlemd  15258  pltfval  15913  pmtrfv  16801  dpjidcl  17427  isirred  17668  isdrng2  17726  drngmcl  17729  drngid2  17732  isdrngd  17741  lssset  17900  xrs1mnd  18776  xrs1cmn  18778  xrge0subm  18779  cnmsubglem  18800  islindf4  19165  smadiadetlem1a  19457  basdif0  19746  tgdif0  19786  clsval2  19843  neitr  19974  lecldbas  20013  pnrmopn  20137  cmpcld  20195  cmpfi  20201  csdfil  20687  ufileu  20712  filufint  20713  alexsublem  20836  ptcmplem2  20845  xrge0gsumle  21630  xrge0tsms  21631  bcth3  22062  iunmbl  22255  i1fd  22380  tdeglem4  22750  reefgim  23137  logbmpt  23455  logbfval  23457  axlowdimlem15  24676  axlowdim  24681  elntg  24704  usgrares1  24827  cusgrares  24889  cusgrafilem3  24898  nbhashuvtx1  25332  frgrawopreglem1  25461  ablomul  25771  eigvecval  27228  elpwdifcl  27836  disjdifprg  27867  padct  27992  resf1o  28000  xrge00  28126  xrge0tsmsd  28228  locfinref  28297  esummono  28501  esumpad  28502  esumpad2  28503  insiga  28585  ldsysgenld  28608  sigapildsys  28610  carsgclctun  28769  sitgclg  28790  ballotlemfrc  28971  ballotlem8  28981  bnj852  29306  bnj865  29308  subfacp1lem5  29481  iscvm  29556  cvmsval  29563  mdvval  29716  topdifinffinlem  31264  voliunnfl  31430  fdc  31520  isdrngo2  31643  watvalN  33010  hvmapfval  34779  lzenom  35064  diophin  35067  diophren  35108  cntzsdrg  35515  deg1mhm  35531  ssdifcl  35622  sssymdifcl  35623  stoweidlem57  37207  fourierdlem102  37359  fourierdlem114  37371  usgresvm1  38072  usgresvm1ALT  38076  lincdifsn  38536  lindslinindsimp1  38569  lindslinindimp2lem2  38571  lindslinindimp2lem4  38573  lindslinindsimp2lem5  38574  lindslinindsimp2  38575  lincresunit1  38589  lincresunit2  38590  lincresunit3lem2  38592  lincresunit3  38593
  Copyright terms: Public domain W3C validator