Theorem difexg 5276

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ∖ cdif 3900   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920

This theorem is referenced by:  difexi  5277  difexd  5278  difex2  7715  elpwun  7724  2oconcl  8440  fnoe  8447  difsnen  8999  fodomr  9068  domss2  9076  domssex2  9077  domssex  9078  limenpsi  9092  dif1enlem  9096  sucdom2  9139  brwdom2  9490  infeq5i  9557  infdifsn  9578  dfac8clem  9954  ssfin4  10232  isf34lem1  10294  compssiso  10296  fin1a2lem7  10328  fin1a2lem13  10334  fpwwe2lem12  10565  hashgt23el  14359  pmtrfv  19393  isirred  20367  isdrng2  20688  drngmclOLD  20696  drngid2  20697  isdrngd  20710  isdrngdOLD  20712  subdrgint  20748  cnmsubglem  21397  islindf4  21805  smadiadetlem1a  22619  basdif0  22909  tgdif0  22948  clsval2  23006  cmpcld  23358  ptcmplem2  24009  iunmbl  25522  logbfval  26768  nbfusgrlevtxm2  29463  vtxdginducedm1  29629  frgrwopreglem1  30399  eigvecval  31983  elpwdifcl  32612  disjdifprg  32661  mptiffisupp  32782  padct  32807  resf1o  32819  xrge00  33106  xrge0tsmsd  33166  tocycf  33210  ist0cld  34010  locfinref  34018  ldsysgenld  34337  sigapildsys  34339  carsgclctun  34498  sitgclg  34519  ballotlemfrc  34704  ballotlem8  34714  bnj852  35096  bnj865  35098  subfacp1lem5  35397  iscvm  35472  cvmsval  35479  mdvval  35717  topdifinffinlem  37599  pibt2  37669  poimirlem15  37883  voliunnfl  37912  fdc  37993  isdrngo2  38206  lzenom  43124  diophin  43126  diophren  43167  deg1mhm  43554  stoweidlem57  46412  fourierdlem102  46563  fourierdlem114  46575  pwsal  46670  gsumge0cl  46726  caragendifcl  46869  carageniuncllem1  46876  isomenndlem  46885  hoidmv1lelem2  46947  lincdifsn  48781  lindslinindsimp1  48814  lindslinindimp2lem2  48816  lindslinindimp2lem4  48818  lindslinindsimp2lem5  48819  lindslinindsimp2  48820  lincresunit1  48834  lincresunit2  48835  lincresunit3lem2  48837  lincresunit3  48838