Theorem difexg 5287

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3914   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934

This theorem is referenced by:  difexi  5288  difexd  5289  difex2  7739  elpwun  7748  2oconcl  8470  fnoe  8477  difsnen  9027  sucdom2OLD  9056  fodomr  9098  domss2  9106  domssex2  9107  domssex  9108  limenpsi  9122  dif1enlem  9126  sucdom2  9173  brwdom2  9533  infeq5i  9596  infdifsn  9617  dfac8clem  9992  ssfin4  10270  isf34lem1  10332  compssiso  10334  fin1a2lem7  10366  fin1a2lem13  10372  fpwwe2lem12  10602  hashgt23el  14396  pmtrfv  19389  isirred  20335  isdrng2  20659  drngmclOLD  20667  drngid2  20668  isdrngd  20681  isdrngdOLD  20683  subdrgint  20719  cnmsubglem  21354  islindf4  21754  smadiadetlem1a  22557  basdif0  22847  tgdif0  22886  clsval2  22944  cmpcld  23296  ptcmplem2  23947  iunmbl  25461  logbfval  26707  nbfusgrlevtxm2  29312  vtxdginducedm1  29478  frgrwopreglem1  30248  eigvecval  31832  elpwdifcl  32462  disjdifprg  32511  mptiffisupp  32623  padct  32650  resf1o  32660  xrge00  32960  xrge0tsmsd  33009  tocycf  33081  ist0cld  33830  locfinref  33838  ldsysgenld  34157  sigapildsys  34159  carsgclctun  34319  sitgclg  34340  ballotlemfrc  34525  ballotlem8  34535  bnj852  34918  bnj865  34920  subfacp1lem5  35178  iscvm  35253  cvmsval  35260  mdvval  35498  topdifinffinlem  37342  pibt2  37412  poimirlem15  37636  voliunnfl  37665  fdc  37746  isdrngo2  37959  lzenom  42765  diophin  42767  diophren  42808  deg1mhm  43196  stoweidlem57  46062  fourierdlem102  46213  fourierdlem114  46225  pwsal  46320  gsumge0cl  46376  caragendifcl  46519  carageniuncllem1  46526  isomenndlem  46535  hoidmv1lelem2  46597  lincdifsn  48417  lindslinindsimp1  48450  lindslinindimp2lem2  48452  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lincresunit1  48470  lincresunit2  48471  lincresunit3lem2  48473  lincresunit3  48474