Theorem difexg 5291

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916

This theorem is used by:  difexi  5292  difexd  5293  difex2  7772  elpwun  7781  2oconcl  8504  fnoe  8511  difsnen  9071  fodomr  9140  domss2  9148  domssex2  9149  domssex  9150  limenpsi  9164  dif1enlem  9168  sucdom2  9211  brwdom2  9560  infeq5i  9630  infdifsn  9651  dfac8clem  10104  ssfin4  10381  isf34lem1  10443  compssiso  10445  fin1a2lem7  10477  fin1a2lem13  10483  fpwwe2lem12  10720  hashgt23el  14562  pmtrfv  19659  isirred  20642  isdrng2  20990  drngid2  21003  isdrngd  21015  isdrngdOLD  21017  subdrgint  21053  cnmsubglem  21729  islindf4  22137  smadiadetlem1a  22971  basdif0  23264  tgdif0  23303  clsval2  23361  cmpcld  23713  ptcmplem2  24365  iunmbl  25867  logbfval  27111  nbfusgrlevtxm2  29952  vtxdginducedm1  30117  frgrwopreglem1  30906  eigvecval  32491  elpwdifcl  33115  disjdifprg  33162  mptiffisupp  33279  resf1o  33315  xrge00  33568  xrge0tsmsd  33627  tocycf  33671  ist0cld  34458  locfinref  34466  ldsysgenld  34786  sigapildsys  34788  carsgclctun  34946  sitgclg  34967  ballotlemfrc  35152  ballotlem8  35162  bnj852  35544  bnj865  35546  subfacp1lem5  35928  iscvm  36003  cvmsval  36010  mdvval  36248  ttcwf2  37293  topdifinffinlem  38250  pibt2  38320  poimirlem15  38533  voliunnfl  38562  fdc  38659  isdrngo2  38872  lzenom  43760  diophin  43762  diophren  43799  deg1mhm  44186  stoweidlem57  47036  fourierdlem102  47187  fourierdlem114  47199  pwsal  47294  gsumge0cl  47350  caragendifcl  47493  carageniuncllem1  47500  isomenndlem  47509  hoidmv1lelem2  47571  lincdifsn  49505  lindslinindsimp1  49538  lindslinindimp2lem2  49540  lindslinindimp2lem4  49542  lindslinindsimp2lem5  49543  lindslinindsimp2  49544  lincresunit1  49558  lincresunit2  49559  lincresunit3lem2  49561  lincresunit3  49562