Theorem difexg 5347

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993

This theorem is referenced by:  difexi  5348  difexd  5349  difex2  7795  elpwun  7804  2oconcl  8559  fnoe  8566  difsnen  9119  sucdom2OLD  9148  fodomr  9194  domss2  9202  domssex2  9203  domssex  9204  limenpsi  9218  dif1enlem  9222  sucdom2  9269  brwdom2  9642  infeq5i  9705  infdifsn  9726  dfac8clem  10101  ssfin4  10379  isf34lem1  10441  compssiso  10443  fin1a2lem7  10475  fin1a2lem13  10481  fpwwe2lem12  10711  hashgt23el  14473  pmtrfv  19494  isirred  20445  isdrng2  20765  drngmclOLD  20773  drngid2  20774  isdrngd  20787  isdrngdOLD  20789  subdrgint  20826  cnmsubglem  21471  islindf4  21881  smadiadetlem1a  22690  basdif0  22981  tgdif0  23020  clsval2  23079  cmpcld  23431  ptcmplem2  24082  iunmbl  25607  logbfval  26851  nbfusgrlevtxm2  29413  vtxdginducedm1  29579  frgrwopreglem1  30344  eigvecval  31928  elpwdifcl  32556  disjdifprg  32597  mptiffisupp  32705  padct  32733  resf1o  32744  xrge00  32998  xrge0tsmsd  33041  tocycf  33110  ist0cld  33779  locfinref  33787  ldsysgenld  34124  sigapildsys  34126  carsgclctun  34286  sitgclg  34307  ballotlemfrc  34491  ballotlem8  34501  bnj852  34897  bnj865  34899  subfacp1lem5  35152  iscvm  35227  cvmsval  35234  mdvval  35472  topdifinffinlem  37313  pibt2  37383  poimirlem15  37595  voliunnfl  37624  fdc  37705  isdrngo2  37918  lzenom  42726  diophin  42728  diophren  42769  deg1mhm  43161  stoweidlem57  45978  fourierdlem102  46129  fourierdlem114  46141  pwsal  46236  gsumge0cl  46292  caragendifcl  46435  carageniuncllem1  46442  isomenndlem  46451  hoidmv1lelem2  46513  lincdifsn  48153  lindslinindsimp1  48186  lindslinindimp2lem2  48188  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lincresunit1  48206  lincresunit2  48207  lincresunit3lem2  48209  lincresunit3  48210