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

Theorem difexg 4570
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 3593 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4568 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 675 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1869   _Vcvv 3082    \ cdif 3434    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-dif 3440  df-in 3444  df-ss 3451
This theorem is referenced by:  difex2  6610  elpwun  6616  2oconcl  7211  fnoe  7218  ralxpmap  7527  difsnen  7658  domdifsn  7659  domunsncan  7676  fodomr  7727  domss2  7735  domssex2  7736  domssex  7737  mapdom2  7747  limenpsi  7751  sucdom2  7772  findcard  7814  findcard2  7815  frfi  7820  unfilem3  7841  marypha1lem  7951  brwdom2  8092  infeq5i  8145  infdifsn  8165  dfac8clem  8465  acni  8478  dfac9  8568  dfacacn  8573  kmlem11  8592  kmlem12  8593  infpss  8649  ssfin4  8742  fin23lem28  8772  isf32lem6  8790  isf32lem7  8791  isf32lem8  8792  isf34lem1  8804  compssiso  8806  enfin1ai  8816  fin1a2lem7  8838  fin1a2lem13  8844  axdc2lem  8880  axcclem  8889  zornn0g  8937  fpwwe2lem13  9069  fpwwe2  9070  canthp1lem1  9079  grothprim  9261  hashbclem  12614  hashf1lem1  12617  fi1uzind  12648  brfi1uzind  12649  brfi1indALT  12651  opfi1uzind  12652  ramub1lem1  14977  mrieqv2d  15538  mreexexlemd  15543  pltfval  16198  pmtrfv  17086  dpjidcl  17684  isirred  17920  isdrng2  17978  drngmcl  17981  drngid2  17984  isdrngd  17993  lssset  18150  xrs1mnd  18999  xrs1cmn  19001  xrge0subm  19002  cnmsubglem  19023  islindf4  19388  smadiadetlem1a  19680  basdif0  19960  tgdif0  20000  clsval2  20057  neitr  20188  lecldbas  20227  pnrmopn  20351  cmpcld  20409  cmpfi  20415  csdfil  20901  ufileu  20926  filufint  20927  alexsublem  21051  ptcmplem2  21060  xrge0gsumle  21843  xrge0tsms  21844  bcth3  22291  iunmbl  22498  i1fd  22631  tdeglem4  23001  reefgim  23397  logbmpt  23717  logbfval  23719  axlowdimlem15  24978  axlowdim  24983  elntg  25006  usgrares1  25130  cusgrares  25192  cusgrafilem3  25201  nbhashuvtx1  25635  frgrawopreglem1  25764  ablomul  26075  eigvecval  27541  elpwdifcl  28150  disjdifprg  28181  padct  28307  resf1o  28315  xrge00  28449  xrge0tsmsd  28550  locfinref  28670  esummono  28877  esumpad  28878  esumpad2  28879  insiga  28961  ldsysgenld  28984  sigapildsys  28986  carsgclctun  29155  sitgclg  29177  ballotlemfrc  29361  ballotlem8  29371  ballotlemfrcOLD  29399  ballotlem8OLD  29409  bnj852  29734  bnj865  29736  subfacp1lem5  29909  iscvm  29984  cvmsval  29991  mdvval  30144  topdifinffinlem  31708  poimirlem15  31913  voliunnfl  31942  fdc  32032  isdrngo2  32155  watvalN  33521  hvmapfval  35290  lzenom  35575  diophin  35578  diophren  35619  cntzsdrg  36032  deg1mhm  36048  ssdifcl  36139  sssymdifcl  36140  stoweidlem57  37782  fourierdlem102  37936  fourierdlem114  37948  pwsal  38021  intsal  38034  gsumge0cl  38045  sge0ss  38086  sge0fodjrnlem  38090  iundjiunlem  38120  iundjiun  38121  meaiunlelem  38129  caragendifcl  38158  carageniuncllem1  38165  isomenndlem  38174  usgrres1  38999  usgresvm1  39097  usgresvm1ALT  39101  lincdifsn  39561  lindslinindsimp1  39594  lindslinindimp2lem2  39596  lindslinindimp2lem4  39598  lindslinindsimp2lem5  39599  lindslinindsimp2  39600  lincresunit1  39614  lincresunit2  39615  lincresunit3lem2  39617  lincresunit3  39618
  Copyright terms: Public domain W3C validator