Theorem difexg 5274

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 4088	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5268	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ∖ cdif 3898   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908  df-ss 3918

This theorem is referenced by:  difexi  5275  difexd  5276  difex2  7705  elpwun  7714  2oconcl  8430  fnoe  8437  difsnen  8987  fodomr  9056  domss2  9064  domssex2  9065  domssex  9066  limenpsi  9080  dif1enlem  9084  sucdom2  9127  brwdom2  9478  infeq5i  9545  infdifsn  9566  dfac8clem  9942  ssfin4  10220  isf34lem1  10282  compssiso  10284  fin1a2lem7  10316  fin1a2lem13  10322  fpwwe2lem12  10553  hashgt23el  14347  pmtrfv  19381  isirred  20355  isdrng2  20676  drngmclOLD  20684  drngid2  20685  isdrngd  20698  isdrngdOLD  20700  subdrgint  20736  cnmsubglem  21385  islindf4  21793  smadiadetlem1a  22607  basdif0  22897  tgdif0  22936  clsval2  22994  cmpcld  23346  ptcmplem2  23997  iunmbl  25510  logbfval  26756  nbfusgrlevtxm2  29451  vtxdginducedm1  29617  frgrwopreglem1  30387  eigvecval  31971  elpwdifcl  32601  disjdifprg  32650  mptiffisupp  32772  padct  32797  resf1o  32809  xrge00  33096  xrge0tsmsd  33155  tocycf  33199  ist0cld  33990  locfinref  33998  ldsysgenld  34317  sigapildsys  34319  carsgclctun  34478  sitgclg  34499  ballotlemfrc  34684  ballotlem8  34694  bnj852  35077  bnj865  35079  subfacp1lem5  35378  iscvm  35453  cvmsval  35460  mdvval  35698  topdifinffinlem  37552  pibt2  37622  poimirlem15  37836  voliunnfl  37865  fdc  37946  isdrngo2  38159  lzenom  43012  diophin  43014  diophren  43055  deg1mhm  43442  stoweidlem57  46301  fourierdlem102  46452  fourierdlem114  46464  pwsal  46559  gsumge0cl  46615  caragendifcl  46758  carageniuncllem1  46765  isomenndlem  46774  hoidmv1lelem2  46836  lincdifsn  48670  lindslinindsimp1  48703  lindslinindimp2lem2  48705  lindslinindimp2lem4  48707  lindslinindsimp2lem5  48708  lindslinindsimp2  48709  lincresunit1  48723  lincresunit2  48724  lincresunit3lem2  48726  lincresunit3  48727