Theorem difexg 5282

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919

This theorem is referenced by:  difexi  5283  difexd  5284  difex2  7737  elpwun  7746  2oconcl  8465  fnoe  8472  difsnen  9024  fodomr  9093  domss2  9101  domssex2  9102  domssex  9103  limenpsi  9117  dif1enlem  9121  sucdom2  9164  brwdom2  9514  infeq5i  9584  infdifsn  9605  dfac8clem  9981  ssfin4  10260  isf34lem1  10322  compssiso  10324  fin1a2lem7  10356  fin1a2lem13  10362  fpwwe2lem12  10593  hashgt23el  14430  pmtrfv  19482  isirred  20454  isdrng2  20779  drngmclOLD  20787  drngid2  20788  isdrngd  20801  isdrngdOLD  20803  subdrgint  20839  cnmsubglem  21469  islindf4  21877  smadiadetlem1a  22710  basdif0  23000  tgdif0  23039  clsval2  23097  cmpcld  23449  ptcmplem2  24100  iunmbl  25602  logbfval  26842  nbfusgrlevtxm2  29535  vtxdginducedm1  29700  frgrwopreglem1  30470  eigvecval  32055  elpwdifcl  32684  disjdifprg  32734  mptiffisupp  32855  resf1o  32892  xrge00  33152  xrge0tsmsd  33213  tocycf  33257  ist0cld  34090  locfinref  34098  ldsysgenld  34417  sigapildsys  34419  carsgclctun  34578  sitgclg  34599  ballotlemfrc  34784  ballotlem8  34794  bnj852  35176  bnj865  35178  subfacp1lem5  35494  iscvm  35569  cvmsval  35576  mdvval  35814  ttcwf2  36845  topdifinffinlem  37801  pibt2  37871  poimirlem15  38094  voliunnfl  38123  fdc  38204  isdrngo2  38417  lzenom  43311  diophin  43313  diophren  43350  deg1mhm  43737  stoweidlem57  46591  fourierdlem102  46742  fourierdlem114  46754  pwsal  46849  gsumge0cl  46905  caragendifcl  47048  carageniuncllem1  47055  isomenndlem  47064  hoidmv1lelem2  47126  lincdifsn  49006  lindslinindsimp1  49039  lindslinindimp2lem2  49041  lindslinindimp2lem4  49043  lindslinindsimp2lem5  49044  lindslinindsimp2  49045  lincresunit1  49059  lincresunit2  49060  lincresunit3lem2  49062  lincresunit3  49063