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

Theorem difexg 4351
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 3474 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4349 . 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 1725   _Vcvv 2956    \ cdif 3317    C_ wss 3320
This theorem is referenced by:  difex2  4714  elpwun  4756  2oconcl  6747  fnoe  6754  difsnen  7190  domdifsn  7191  domunsncan  7208  fodomr  7258  domss2  7266  domssex2  7267  domssex  7268  mapdom2  7278  limenpsi  7282  sucdom2  7303  findcard  7347  findcard2  7348  frfi  7352  unfilem3  7373  marypha1lem  7438  brwdom2  7541  infeq5i  7591  infdifsn  7611  dfac8clem  7913  acni  7926  dfac9  8016  dfacacn  8021  kmlem11  8040  kmlem12  8041  infpss  8097  ssfin4  8190  fin23lem28  8220  isf32lem6  8238  isf32lem7  8239  isf32lem8  8240  isf34lem1  8252  compssiso  8254  enfin1ai  8264  fin1a2lem7  8286  fin1a2lem13  8292  axdc2lem  8328  axcclem  8337  zornn0g  8385  fpwwe2lem13  8517  fpwwe2  8518  canthp1lem1  8527  grothprim  8709  hashbclem  11701  hashf1lem1  11704  brfi1uzind  11715  ramub1lem1  13394  mrieqv2d  13864  mreexexlemd  13869  pltfval  14416  isirred  15804  isdrng2  15845  drngmcl  15848  drngid2  15851  isdrngd  15860  lssset  16010  xrs1mnd  16736  xrs1cmn  16738  xrge0subm  16739  cnmsubglem  16761  basdif0  17018  tgdif0  17057  clsval2  17114  neitr  17244  lecldbas  17283  pnrmopn  17407  cmpcld  17465  cmpfi  17471  csdfil  17926  ufileu  17951  filufint  17952  alexsublem  18075  ptcmplem2  18084  xrge0gsumle  18864  xrge0tsms  18865  bcth3  19284  iunmbl  19447  i1fd  19573  tdeglem4  19983  reefgim  20366  usgrares1  21424  cusgrares  21481  cusgrafilem3  21490  ablomul  21943  eigvecval  23399  disjdifprg  24017  xrge00  24208  xrge0tsmsd  24223  esummono  24450  gsumesum  24451  insiga  24520  sitgclg  24656  ballotlemfrc  24784  ballotlem8  24794  subfacp1lem5  24870  iscvm  24946  cvmsval  24953  axlowdimlem15  25895  axlowdim  25900  voliunnfl  26250  fdc  26449  isdrngo2  26574  ralxpmap  26742  lzenom  26828  diophin  26831  diophren  26874  islindf4  27285  pmtrfv  27372  cntzsdrg  27487  deg1mhm  27503  stoweidlem57  27782  frgrawopreglem1  28433  bnj852  29292  bnj865  29294  watvalN  30790  hvmapfval  32557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator