Theorem difexg 5328

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3946   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  difexi  5329  difexd  5330  difex2  7747  elpwun  7756  2oconcl  8503  fnoe  8510  difsnen  9053  sucdom2OLD  9082  fodomr  9128  domss2  9136  domssex2  9137  domssex  9138  limenpsi  9152  dif1enlem  9156  sucdom2  9206  brwdom2  9568  infeq5i  9631  infdifsn  9652  dfac8clem  10027  ssfin4  10305  isf34lem1  10367  compssiso  10369  fin1a2lem7  10401  fin1a2lem13  10407  fpwwe2lem12  10637  hashgt23el  14384  hashf1lem1OLD  14416  pmtrfv  19320  isirred  20233  isdrng2  20371  drngmcl  20374  drngid2  20378  isdrngd  20390  isdrngdOLD  20392  subdrgint  20419  cnmsubglem  21008  islindf4  21393  smadiadetlem1a  22165  basdif0  22456  tgdif0  22495  clsval2  22554  cmpcld  22906  ptcmplem2  23557  iunmbl  25070  tdeglem4OLD  25578  logbfval  26295  nbfusgrlevtxm2  28666  vtxdginducedm1  28831  frgrwopreglem1  29596  eigvecval  31180  elpwdifcl  31795  disjdifprg  31837  mptiffisupp  31946  padct  31975  resf1o  31986  xrge00  32218  xrge0tsmsd  32240  tocycf  32307  ist0cld  32844  locfinref  32852  ldsysgenld  33189  sigapildsys  33191  carsgclctun  33351  sitgclg  33372  ballotlemfrc  33556  ballotlem8  33566  bnj852  33963  bnj865  33965  subfacp1lem5  34206  iscvm  34281  cvmsval  34288  mdvval  34526  topdifinffinlem  36276  pibt2  36346  poimirlem15  36551  voliunnfl  36580  fdc  36661  isdrngo2  36874  lzenom  41556  diophin  41558  diophren  41599  deg1mhm  41997  stoweidlem57  44821  fourierdlem102  44972  fourierdlem114  44984  pwsal  45079  gsumge0cl  45135  caragendifcl  45278  carageniuncllem1  45285  isomenndlem  45294  hoidmv1lelem2  45356  lincdifsn  47153  lindslinindsimp1  47186  lindslinindimp2lem2  47188  lindslinindimp2lem4  47190  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  lincresunit1  47206  lincresunit2  47207  lincresunit3lem2  47209  lincresunit3  47210