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

Theorem difexg 4178
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 3316 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4176 . 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 1696   _Vcvv 2801    \ cdif 3162    C_ wss 3165
This theorem is referenced by:  difex2  4541  elpwun  4583  2oconcl  6518  fnoe  6525  difsnen  6960  domdifsn  6961  domunsncan  6978  fodomr  7028  domss2  7036  domssex2  7037  domssex  7038  mapdom2  7048  limenpsi  7052  sucdom2  7073  findcard  7113  findcard2  7114  frfi  7118  unfilem3  7139  marypha1lem  7202  brwdom2  7303  infeq5i  7353  infdifsn  7373  dfac8clem  7675  acni  7688  dfac9  7778  dfacacn  7783  kmlem11  7802  kmlem12  7803  infpss  7859  ssfin4  7952  fin23lem28  7982  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  isf34lem1  8014  compssiso  8016  enfin1ai  8026  fin1a2lem7  8048  fin1a2lem13  8054  axdc2lem  8090  axcclem  8099  zornn0g  8148  fpwwe2lem13  8280  fpwwe2  8281  canthp1lem1  8290  grothprim  8472  hashbclem  11406  hashf1lem1  11409  ramub1lem1  13089  mrieqv2d  13557  mreexexlemd  13562  pltfval  14109  isirred  15497  isdrng2  15538  drngmcl  15541  drngid2  15544  isdrngd  15553  lssset  15707  xrs1mnd  16425  xrs1cmn  16427  xrge0subm  16428  cnmsubglem  16450  basdif0  16707  tgdif0  16746  clsval2  16803  lecldbas  16965  pnrmopn  17087  cmpcld  17145  cmpfi  17151  csdfil  17605  ufileu  17630  filufint  17631  alexsublem  17754  ptcmplem2  17763  xrge0gsumle  18354  xrge0tsms  18355  bcth3  18769  iunmbl  18926  i1fd  19052  tdeglem4  19462  reefgim  19842  ablomul  21038  eigvecval  22492  ballotlemfrc  23101  ballotlem8  23111  xrge00  23326  disjdifprg  23367  xrge0tsmsd  23397  pwsiga  23506  insiga  23513  subfacp1lem5  23730  iscvm  23805  cvmsval  23812  axlowdimlem15  24655  axlowdim  24660  isdivcv2  25795  isside0  26266  pdiveql  26270  aishp  26274  bhp3  26279  fdc  26557  isdrngo2  26691  ralxpmap  26863  lzenom  26951  diophin  26954  diophren  26998  islindf4  27410  pmtrfv  27497  cntzsdrg  27612  deg1mhm  27628  stoweidlem57  27908  bnj852  29268  bnj865  29270  watvalN  30804  hvmapfval  32571
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator