Theorem difexg 5262

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ∖ cdif 3894   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-in 3904  df-ss 3914

This theorem is referenced by:  difexi  5263  difexd  5264  difex2  7688  elpwun  7697  2oconcl  8413  fnoe  8420  difsnen  8967  fodomr  9036  domss2  9044  domssex2  9045  domssex  9046  limenpsi  9060  dif1enlem  9064  sucdom2  9107  brwdom2  9454  infeq5i  9521  infdifsn  9542  dfac8clem  9918  ssfin4  10196  isf34lem1  10258  compssiso  10260  fin1a2lem7  10292  fin1a2lem13  10298  fpwwe2lem12  10528  hashgt23el  14326  pmtrfv  19359  isirred  20332  isdrng2  20653  drngmclOLD  20661  drngid2  20662  isdrngd  20675  isdrngdOLD  20677  subdrgint  20713  cnmsubglem  21362  islindf4  21770  smadiadetlem1a  22573  basdif0  22863  tgdif0  22902  clsval2  22960  cmpcld  23312  ptcmplem2  23963  iunmbl  25476  logbfval  26722  nbfusgrlevtxm2  29351  vtxdginducedm1  29517  frgrwopreglem1  30284  eigvecval  31868  elpwdifcl  32498  disjdifprg  32547  mptiffisupp  32666  padct  32693  resf1o  32705  xrge00  32987  xrge0tsmsd  33034  tocycf  33078  ist0cld  33838  locfinref  33846  ldsysgenld  34165  sigapildsys  34167  carsgclctun  34326  sitgclg  34347  ballotlemfrc  34532  ballotlem8  34542  bnj852  34925  bnj865  34927  subfacp1lem5  35220  iscvm  35295  cvmsval  35302  mdvval  35540  topdifinffinlem  37381  pibt2  37451  poimirlem15  37675  voliunnfl  37704  fdc  37785  isdrngo2  37998  lzenom  42803  diophin  42805  diophren  42846  deg1mhm  43233  stoweidlem57  46095  fourierdlem102  46246  fourierdlem114  46258  pwsal  46353  gsumge0cl  46409  caragendifcl  46552  carageniuncllem1  46559  isomenndlem  46568  hoidmv1lelem2  46630  lincdifsn  48456  lindslinindsimp1  48489  lindslinindimp2lem2  48491  lindslinindimp2lem4  48493  lindslinindsimp2lem5  48494  lindslinindsimp2  48495  lincresunit1  48509  lincresunit2  48510  lincresunit3lem2  48512  lincresunit3  48513