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

Theorem difexg 4352
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 3475 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4350 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 653 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   _Vcvv 2957    \ cdif 3318    C_ wss 3321
This theorem is referenced by:  difex2  4715  elpwun  4757  2oconcl  6748  fnoe  6755  difsnen  7191  domdifsn  7192  domunsncan  7209  fodomr  7259  domss2  7267  domssex2  7268  domssex  7269  mapdom2  7279  limenpsi  7283  sucdom2  7304  findcard  7348  findcard2  7349  frfi  7353  unfilem3  7374  marypha1lem  7439  brwdom2  7542  infeq5i  7592  infdifsn  7612  dfac8clem  7914  acni  7927  dfac9  8017  dfacacn  8022  kmlem11  8041  kmlem12  8042  infpss  8098  ssfin4  8191  fin23lem28  8221  isf32lem6  8239  isf32lem7  8240  isf32lem8  8241  isf34lem1  8253  compssiso  8255  enfin1ai  8265  fin1a2lem7  8287  fin1a2lem13  8293  axdc2lem  8329  axcclem  8338  zornn0g  8386  fpwwe2lem13  8518  fpwwe2  8519  canthp1lem1  8528  grothprim  8710  hashbclem  11702  hashf1lem1  11705  brfi1uzind  11716  ramub1lem1  13395  mrieqv2d  13865  mreexexlemd  13870  pltfval  14417  isirred  15805  isdrng2  15846  drngmcl  15849  drngid2  15852  isdrngd  15861  lssset  16011  xrs1mnd  16737  xrs1cmn  16739  xrge0subm  16740  cnmsubglem  16762  basdif0  17019  tgdif0  17058  clsval2  17115  neitr  17245  lecldbas  17284  pnrmopn  17408  cmpcld  17466  cmpfi  17472  csdfil  17927  ufileu  17952  filufint  17953  alexsublem  18076  ptcmplem2  18085  xrge0gsumle  18865  xrge0tsms  18866  bcth3  19285  iunmbl  19448  i1fd  19574  tdeglem4  19984  reefgim  20367  usgrares1  21425  cusgrares  21482  cusgrafilem3  21491  ablomul  21944  eigvecval  23400  disjdifprg  24018  xrge00  24209  xrge0tsmsd  24224  esummono  24451  gsumesum  24452  insiga  24521  sitgclg  24657  ballotlemfrc  24785  ballotlem8  24795  subfacp1lem5  24871  iscvm  24947  cvmsval  24954  axlowdimlem15  25896  axlowdim  25901  voliunnfl  26251  fdc  26450  isdrngo2  26575  ralxpmap  26743  lzenom  26829  diophin  26832  diophren  26875  islindf4  27286  pmtrfv  27373  cntzsdrg  27488  deg1mhm  27504  stoweidlem57  27783  frgrawopreglem1  28434  bnj852  29293  bnj865  29295  watvalN  30791  hvmapfval  32558
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-dif 3324  df-in 3328  df-ss 3335
  Copyright terms: Public domain W3C validator