Theorem difexg 5301

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ∖ cdif 3903   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-in 3913  df-ss 3923

This theorem is referenced by:  difexi  5302  difexd  5303  difex2  7760  elpwun  7769  2oconcl  8489  fnoe  8496  difsnen  9048  fodomr  9117  domss2  9125  domssex2  9126  domssex  9127  limenpsi  9141  dif1enlem  9145  sucdom2  9188  brwdom2  9536  infeq5i  9606  infdifsn  9627  dfac8clem  10017  ssfin4  10295  isf34lem1  10357  compssiso  10359  fin1a2lem7  10391  fin1a2lem13  10397  fpwwe2lem12  10628  hashgt23el  14463  pmtrfv  19523  isirred  20502  isdrng2  20830  drngid2  20838  isdrngd  20850  isdrngdOLD  20852  subdrgint  20887  cnmsubglem  21561  islindf4  21969  smadiadetlem1a  22801  basdif0  23091  tgdif0  23130  clsval2  23188  cmpcld  23540  ptcmplem2  24191  iunmbl  25693  logbfval  26936  nbfusgrlevtxm2  29709  vtxdginducedm1  29874  frgrwopreglem1  30644  eigvecval  32229  elpwdifcl  32853  disjdifprg  32901  mptiffisupp  33019  resf1o  33056  xrge00  33315  xrge0tsmsd  33374  tocycf  33418  ist0cld  34204  locfinref  34212  ldsysgenld  34531  sigapildsys  34533  carsgclctun  34692  sitgclg  34713  ballotlemfrc  34898  ballotlem8  34908  bnj852  35290  bnj865  35292  subfacp1lem5  35657  iscvm  35732  cvmsval  35739  mdvval  35977  ttcwf2  37017  topdifinffinlem  37974  pibt2  38044  poimirlem15  38267  voliunnfl  38296  fdc  38377  isdrngo2  38590  lzenom  43484  diophin  43486  diophren  43523  deg1mhm  43910  stoweidlem57  46754  fourierdlem102  46905  fourierdlem114  46917  pwsal  47012  gsumge0cl  47068  caragendifcl  47211  carageniuncllem1  47218  isomenndlem  47227  hoidmv1lelem2  47289  lincdifsn  49187  lindslinindsimp1  49220  lindslinindimp2lem2  49222  lindslinindimp2lem4  49224  lindslinindsimp2lem5  49225  lindslinindsimp2  49226  lincresunit1  49240  lincresunit2  49241  lincresunit3lem2  49243  lincresunit3  49244