Theorem difexg 4808

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

Step	Hyp	Ref	Expression
1		difss 3737	. 2 |- ( A \ B ) C_ A
2		ssexg 4804	. 2 |- ( ( ( A \ B ) C_ A /\ A e. V ) -> ( A \ B ) e. _V )
3	1, 2	mpan 706	1 |- ( A e. V -> ( A \ B ) e. _V )

Syntax hints:   -> wi 4   e. wcel 1990   _Vcvv 3200   \ cdif 3571   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  difexi  4809  difexOLD  4810  difex2  6969  elpwun  6977  2oconcl  7583  fnoe  7590  ralxpmap  7907  difsnen  8042  domdifsn  8043  domunsncan  8060  fodomr  8111  domss2  8119  domssex2  8120  domssex  8121  mapdom2  8131  limenpsi  8135  sucdom2  8156  findcard  8199  findcard2  8200  frfi  8205  unfilem3  8226  brwdom2  8478  infeq5i  8533  infdifsn  8554  dfac8clem  8855  acni  8868  dfac9  8958  dfacacn  8963  infpss  9039  ssfin4  9132  fin23lem28  9162  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  isf34lem1  9194  compssiso  9196  enfin1ai  9206  fin1a2lem7  9228  fin1a2lem13  9234  axdc2lem  9270  axcclem  9279  zornn0g  9327  fpwwe2lem13  9464  fpwwe2  9465  canthp1lem1  9474  grothprim  9656  hashbclem  13236  hashf1lem1  13239  fi1uzind  13279  brfi1uzind  13280  brfi1indALT  13282  fi1uzindOLD  13285  brfi1uzindOLD  13286  brfi1indALTOLD  13288  opfi1uzindOLD  13289  ramub1lem1  15730  mrieqv2d  16299  mreexexlemd  16304  pltfval  16959  pmtrfv  17872  dpjidcl  18457  isirred  18699  isdrng2  18757  drngmcl  18760  drngid2  18763  isdrngd  18772  lssset  18934  xrs1mnd  19784  xrs1cmn  19786  xrge0subm  19787  cnmsubglem  19809  islindf4  20177  smadiadetlem1a  20469  basdif0  20757  tgdif0  20796  clsval2  20854  neitr  20984  lecldbas  21023  pnrmopn  21147  cmpcld  21205  cmpfi  21211  csdfil  21698  ufileu  21723  filufint  21724  alexsublem  21848  ptcmplem2  21857  xrge0gsumle  22636  xrge0tsms  22637  bcth3  23128  iunmbl  23321  i1fd  23448  tdeglem4  23820  reefgim  24204  logbmpt  24526  logbfval  24528  axlowdimlem15  25836  axlowdim  25841  elntg  25864  nbfusgrlevtxm1  26279  nbfusgrlevtxm2  26280  cusgrfilem3  26353  vtxdginducedm1  26439  frgrwopreglem1  27176  eigvecval  28755  elpwdifcl  29358  disjdifprg  29388  padct  29497  resf1o  29505  xrge00  29686  xrge0tsmsd  29785  locfinref  29908  esummono  30116  esumpad  30117  esumpad2  30118  insiga  30200  ldsysgenld  30223  sigapildsys  30225  carsgclctun  30383  sitgclg  30404  ballotlemfrc  30588  ballotlem8  30598  bnj852  30991  bnj865  30993  subfacp1lem5  31166  iscvm  31241  cvmsval  31248  mdvval  31401  topdifinffinlem  33195  poimirlem15  33424  voliunnfl  33453  fdc  33541  isdrngo2  33757  watvalN  35279  hvmapfval  37048  lzenom  37333  diophin  37336  diophren  37377  cntzsdrg  37772  deg1mhm  37785  sssymdifcl  37877  clcnvlem  37930  dssmapfv3d  38313  dssmapnvod  38314  ovolsplit  40205  stoweidlem57  40274  fourierdlem102  40425  fourierdlem114  40437  pwsal  40535  intsal  40548  gsumge0cl  40588  sge0ss  40629  sge0fodjrnlem  40633  iundjiunlem  40676  iundjiun  40677  meaiunlelem  40685  caragendifcl  40728  carageniuncllem1  40735  isomenndlem  40744  hoidmv1lelem2  40806  lincdifsn  42213  lindslinindsimp1  42246  lindslinindimp2lem2  42248  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lincresunit1  42266  lincresunit2  42267  lincresunit3lem2  42269  lincresunit3  42270