Theorem difexg 5251

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432   ∖ cdif 3884   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  difexi  5252  difexd  5253  difex2  7610  elpwun  7619  2oconcl  8333  fnoe  8340  difsnen  8840  sucdom2OLD  8869  fodomr  8915  domss2  8923  domssex2  8924  domssex  8925  limenpsi  8939  sucdom2  8989  brwdom2  9332  infeq5i  9394  infdifsn  9415  dfac8clem  9788  ssfin4  10066  isf34lem1  10128  compssiso  10130  fin1a2lem7  10162  fin1a2lem13  10168  fpwwe2lem12  10398  hashgt23el  14139  hashf1lem1OLD  14169  pmtrfv  19060  isirred  19941  isdrng2  20001  drngmcl  20004  drngid2  20007  isdrngd  20016  subdrgint  20071  cnmsubglem  20661  islindf4  21045  smadiadetlem1a  21812  basdif0  22103  tgdif0  22142  clsval2  22201  cmpcld  22553  ptcmplem2  23204  iunmbl  24717  tdeglem4OLD  25225  logbfval  25940  nbfusgrlevtxm2  27745  vtxdginducedm1  27910  frgrwopreglem1  28676  eigvecval  30258  elpwdifcl  30875  disjdifprg  30914  padct  31054  resf1o  31065  xrge00  31295  xrge0tsmsd  31317  tocycf  31384  ist0cld  31783  locfinref  31791  ldsysgenld  32128  sigapildsys  32130  carsgclctun  32288  sitgclg  32309  ballotlemfrc  32493  ballotlem8  32503  bnj852  32901  bnj865  32903  subfacp1lem5  33146  iscvm  33221  cvmsval  33228  mdvval  33466  topdifinffinlem  35518  pibt2  35588  poimirlem15  35792  voliunnfl  35821  fdc  35903  isdrngo2  36116  lzenom  40592  diophin  40594  diophren  40635  deg1mhm  41032  stoweidlem57  43598  fourierdlem102  43749  fourierdlem114  43761  pwsal  43856  gsumge0cl  43909  caragendifcl  44052  carageniuncllem1  44059  isomenndlem  44068  hoidmv1lelem2  44130  lincdifsn  45765  lindslinindsimp1  45798  lindslinindimp2lem2  45800  lindslinindimp2lem4  45802  lindslinindsimp2lem5  45803  lindslinindsimp2  45804  lincresunit1  45818  lincresunit2  45819  lincresunit3lem2  45821  lincresunit3  45822