Theorem difexg 5286

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3913   ⊆ wss 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-in 3923  df-ss 3933

This theorem is referenced by:  difexi  5287  difexd  5288  difex2  7738  elpwun  7747  2oconcl  8469  fnoe  8476  difsnen  9026  sucdom2OLD  9055  fodomr  9097  domss2  9105  domssex2  9106  domssex  9107  limenpsi  9121  dif1enlem  9125  sucdom2  9172  brwdom2  9532  infeq5i  9595  infdifsn  9616  dfac8clem  9991  ssfin4  10269  isf34lem1  10331  compssiso  10333  fin1a2lem7  10365  fin1a2lem13  10371  fpwwe2lem12  10601  hashgt23el  14395  pmtrfv  19388  isirred  20334  isdrng2  20658  drngmclOLD  20666  drngid2  20667  isdrngd  20680  isdrngdOLD  20682  subdrgint  20718  cnmsubglem  21353  islindf4  21753  smadiadetlem1a  22556  basdif0  22846  tgdif0  22885  clsval2  22943  cmpcld  23295  ptcmplem2  23946  iunmbl  25460  logbfval  26706  nbfusgrlevtxm2  29311  vtxdginducedm1  29477  frgrwopreglem1  30247  eigvecval  31831  elpwdifcl  32461  disjdifprg  32510  mptiffisupp  32622  padct  32649  resf1o  32659  xrge00  32959  xrge0tsmsd  33008  tocycf  33080  ist0cld  33829  locfinref  33837  ldsysgenld  34156  sigapildsys  34158  carsgclctun  34318  sitgclg  34339  ballotlemfrc  34524  ballotlem8  34534  bnj852  34917  bnj865  34919  subfacp1lem5  35171  iscvm  35246  cvmsval  35253  mdvval  35491  topdifinffinlem  37330  pibt2  37400  poimirlem15  37624  voliunnfl  37653  fdc  37734  isdrngo2  37947  lzenom  42751  diophin  42753  diophren  42794  deg1mhm  43182  stoweidlem57  46048  fourierdlem102  46199  fourierdlem114  46211  pwsal  46306  gsumge0cl  46362  caragendifcl  46505  carageniuncllem1  46512  isomenndlem  46521  hoidmv1lelem2  46583  lincdifsn  48403  lindslinindsimp1  48436  lindslinindimp2lem2  48438  lindslinindimp2lem4  48440  lindslinindsimp2lem5  48441  lindslinindsimp2  48442  lincresunit1  48456  lincresunit2  48457  lincresunit3lem2  48459  lincresunit3  48460