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

Theorem difexg 4294
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 3419 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4292 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 652 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   _Vcvv 2901    \ cdif 3262    C_ wss 3265
This theorem is referenced by:  difex2  4656  elpwun  4698  2oconcl  6685  fnoe  6692  difsnen  7128  domdifsn  7129  domunsncan  7146  fodomr  7196  domss2  7204  domssex2  7205  domssex  7206  mapdom2  7216  limenpsi  7220  sucdom2  7241  findcard  7285  findcard2  7286  frfi  7290  unfilem3  7311  marypha1lem  7375  brwdom2  7476  infeq5i  7526  infdifsn  7546  dfac8clem  7848  acni  7861  dfac9  7951  dfacacn  7956  kmlem11  7975  kmlem12  7976  infpss  8032  ssfin4  8125  fin23lem28  8155  isf32lem6  8173  isf32lem7  8174  isf32lem8  8175  isf34lem1  8187  compssiso  8189  enfin1ai  8199  fin1a2lem7  8221  fin1a2lem13  8227  axdc2lem  8263  axcclem  8272  zornn0g  8320  fpwwe2lem13  8452  fpwwe2  8453  canthp1lem1  8462  grothprim  8644  hashbclem  11630  hashf1lem1  11633  brfi1uzind  11644  ramub1lem1  13323  mrieqv2d  13793  mreexexlemd  13798  pltfval  14345  isirred  15733  isdrng2  15774  drngmcl  15777  drngid2  15780  isdrngd  15789  lssset  15939  xrs1mnd  16661  xrs1cmn  16663  xrge0subm  16664  cnmsubglem  16686  basdif0  16943  tgdif0  16982  clsval2  17039  neitr  17168  lecldbas  17207  pnrmopn  17331  cmpcld  17389  cmpfi  17395  csdfil  17849  ufileu  17874  filufint  17875  alexsublem  17998  ptcmplem2  18007  xrge0gsumle  18737  xrge0tsms  18738  bcth3  19155  iunmbl  19316  i1fd  19442  tdeglem4  19852  reefgim  20235  usgrares1  21292  cusgrares  21349  cusgrafilem3  21358  ablomul  21793  eigvecval  23249  disjdifprg  23863  xrge00  24039  xrge0tsmsd  24054  esummono  24248  gsumesum  24249  insiga  24318  ballotlemfrc  24565  ballotlem8  24575  subfacp1lem5  24651  iscvm  24727  cvmsval  24734  axlowdimlem15  25611  axlowdim  25616  voliunnfl  25957  fdc  26142  isdrngo2  26267  ralxpmap  26435  lzenom  26521  diophin  26524  diophren  26567  islindf4  26979  pmtrfv  27066  cntzsdrg  27181  deg1mhm  27197  stoweidlem57  27476  frgrawopreglem1  27798  bnj852  28632  bnj865  28634  watvalN  30109  hvmapfval  31876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-dif 3268  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator