Theorem difexg 5334

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979

This theorem is referenced by:  difexi  5335  difexd  5336  difex2  7778  elpwun  7787  2oconcl  8539  fnoe  8546  difsnen  9091  sucdom2OLD  9120  fodomr  9166  domss2  9174  domssex2  9175  domssex  9176  limenpsi  9190  dif1enlem  9194  sucdom2  9240  brwdom2  9610  infeq5i  9673  infdifsn  9694  dfac8clem  10069  ssfin4  10347  isf34lem1  10409  compssiso  10411  fin1a2lem7  10443  fin1a2lem13  10449  fpwwe2lem12  10679  hashgt23el  14459  pmtrfv  19484  isirred  20435  isdrng2  20759  drngmclOLD  20767  drngid2  20768  isdrngd  20781  isdrngdOLD  20783  subdrgint  20820  cnmsubglem  21465  islindf4  21875  smadiadetlem1a  22684  basdif0  22975  tgdif0  23014  clsval2  23073  cmpcld  23425  ptcmplem2  24076  iunmbl  25601  logbfval  26847  nbfusgrlevtxm2  29409  vtxdginducedm1  29575  frgrwopreglem1  30340  eigvecval  31924  elpwdifcl  32553  disjdifprg  32594  mptiffisupp  32707  padct  32736  resf1o  32747  xrge00  32999  xrge0tsmsd  33047  tocycf  33119  ist0cld  33793  locfinref  33801  ldsysgenld  34140  sigapildsys  34142  carsgclctun  34302  sitgclg  34323  ballotlemfrc  34507  ballotlem8  34517  bnj852  34913  bnj865  34915  subfacp1lem5  35168  iscvm  35243  cvmsval  35250  mdvval  35488  topdifinffinlem  37329  pibt2  37399  poimirlem15  37621  voliunnfl  37650  fdc  37731  isdrngo2  37944  lzenom  42757  diophin  42759  diophren  42800  deg1mhm  43188  stoweidlem57  46012  fourierdlem102  46163  fourierdlem114  46175  pwsal  46270  gsumge0cl  46326  caragendifcl  46469  carageniuncllem1  46476  isomenndlem  46485  hoidmv1lelem2  46547  lincdifsn  48269  lindslinindsimp1  48302  lindslinindimp2lem2  48304  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lincresunit1  48322  lincresunit2  48323  lincresunit3lem2  48325  lincresunit3  48326