Theorem difexg 4735

Description: Existence of a difference. (Contributed by NM, 26-May-1998.)

Assertion

Ref	Expression
difexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Proof of Theorem difexg

Step	Hyp	Ref	Expression
1		difss 3699	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 4732	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 702	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554

This theorem is referenced by:  difexi  4736  difexOLD  4737  difex2  6863  elpwun  6869  2oconcl  7470  fnoe  7477  ralxpmap  7793  difsnen  7927  domdifsn  7928  domunsncan  7945  fodomr  7996  domss2  8004  domssex2  8005  domssex  8006  mapdom2  8016  limenpsi  8020  sucdom2  8041  findcard  8084  findcard2  8085  frfi  8090  unfilem3  8111  brwdom2  8361  infeq5i  8416  infdifsn  8437  dfac8clem  8738  acni  8751  dfac9  8841  dfacacn  8846  kmlem11  8865  kmlem12  8866  infpss  8922  ssfin4  9015  fin23lem28  9045  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  isf34lem1  9077  compssiso  9079  enfin1ai  9089  fin1a2lem7  9111  fin1a2lem13  9117  axdc2lem  9153  axcclem  9162  zornn0g  9210  fpwwe2lem13  9343  fpwwe2  9344  canthp1lem1  9353  grothprim  9535  hashbclem  13093  hashf1lem1  13096  fi1uzind  13134  brfi1uzind  13135  brfi1indALT  13137  opfi1uzind  13138  fi1uzindOLD  13140  brfi1uzindOLD  13141  brfi1indALTOLD  13143  opfi1uzindOLD  13144  ramub1lem1  15568  mrieqv2d  16122  mreexexlemd  16127  pltfval  16782  pmtrfv  17695  dpjidcl  18280  isirred  18522  isdrng2  18580  drngmcl  18583  drngid2  18586  isdrngd  18595  lssset  18755  xrs1mnd  19603  xrs1cmn  19605  xrge0subm  19606  cnmsubglem  19628  islindf4  19996  smadiadetlem1a  20288  basdif0  20568  tgdif0  20607  clsval2  20664  neitr  20794  lecldbas  20833  pnrmopn  20957  cmpcld  21015  cmpfi  21021  csdfil  21508  ufileu  21533  filufint  21534  alexsublem  21658  ptcmplem2  21667  xrge0gsumle  22444  xrge0tsms  22445  bcth3  22936  iunmbl  23128  i1fd  23254  tdeglem4  23624  reefgim  24008  logbmpt  24326  logbfval  24328  axlowdimlem15  25636  axlowdim  25641  elntg  25664  usgrares1  25939  cusgrares  26001  cusgrafilem3  26009  nbhashuvtx1  26442  frgrawopreglem1  26571  eigvecval  28139  elpwdifcl  28742  disjdifprg  28770  padct  28885  resf1o  28893  xrge00  29017  xrge0tsmsd  29116  locfinref  29236  esummono  29443  esumpad  29444  esumpad2  29445  insiga  29527  ldsysgenld  29550  sigapildsys  29552  carsgclctun  29710  sitgclg  29731  ballotlemfrc  29915  ballotlem8  29925  bnj852  30245  bnj865  30247  subfacp1lem5  30420  iscvm  30495  cvmsval  30502  mdvval  30655  topdifinffinlem  32371  poimirlem15  32594  voliunnfl  32623  fdc  32711  isdrngo2  32927  watvalN  34297  hvmapfval  36066  lzenom  36351  diophin  36354  diophren  36395  cntzsdrg  36791  deg1mhm  36804  ssdifcl  36895  sssymdifcl  36896  clcnvlem  36949  dssmapfv3d  37333  dssmapnvod  37334  ovolsplit  38881  stoweidlem57  38950  fourierdlem102  39101  fourierdlem114  39113  pwsal  39211  intsal  39224  gsumge0cl  39264  sge0ss  39305  sge0fodjrnlem  39309  iundjiunlem  39352  iundjiun  39353  meaiunlelem  39361  caragendifcl  39404  carageniuncllem1  39411  isomenndlem  39420  hoidmv1lelem2  39482  uhgrspan1lem1  40524  nbfusgrlevtxm1  40605  nbfusgrlevtxm2  40606  cusgrfilem3  40673  frgrwopreglem1  41481  lincdifsn  42007  lindslinindsimp1  42040  lindslinindimp2lem2  42042  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lincresunit1  42060  lincresunit2  42061  lincresunit3lem2  42063  lincresunit3  42064