Theorem difexg 5299

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-ss 3943

This theorem is referenced by:  difexi  5300  difexd  5301  difex2  7754  elpwun  7763  2oconcl  8515  fnoe  8522  difsnen  9067  sucdom2OLD  9096  fodomr  9142  domss2  9150  domssex2  9151  domssex  9152  limenpsi  9166  dif1enlem  9170  sucdom2  9217  brwdom2  9587  infeq5i  9650  infdifsn  9671  dfac8clem  10046  ssfin4  10324  isf34lem1  10386  compssiso  10388  fin1a2lem7  10420  fin1a2lem13  10426  fpwwe2lem12  10656  hashgt23el  14442  pmtrfv  19433  isirred  20379  isdrng2  20703  drngmclOLD  20711  drngid2  20712  isdrngd  20725  isdrngdOLD  20727  subdrgint  20763  cnmsubglem  21398  islindf4  21798  smadiadetlem1a  22601  basdif0  22891  tgdif0  22930  clsval2  22988  cmpcld  23340  ptcmplem2  23991  iunmbl  25506  logbfval  26752  nbfusgrlevtxm2  29357  vtxdginducedm1  29523  frgrwopreglem1  30293  eigvecval  31877  elpwdifcl  32507  disjdifprg  32556  mptiffisupp  32670  padct  32697  resf1o  32707  xrge00  33007  xrge0tsmsd  33056  tocycf  33128  ist0cld  33864  locfinref  33872  ldsysgenld  34191  sigapildsys  34193  carsgclctun  34353  sitgclg  34374  ballotlemfrc  34559  ballotlem8  34569  bnj852  34952  bnj865  34954  subfacp1lem5  35206  iscvm  35281  cvmsval  35288  mdvval  35526  topdifinffinlem  37365  pibt2  37435  poimirlem15  37659  voliunnfl  37688  fdc  37769  isdrngo2  37982  lzenom  42793  diophin  42795  diophren  42836  deg1mhm  43224  stoweidlem57  46086  fourierdlem102  46237  fourierdlem114  46249  pwsal  46344  gsumge0cl  46400  caragendifcl  46543  carageniuncllem1  46550  isomenndlem  46559  hoidmv1lelem2  46621  lincdifsn  48400  lindslinindsimp1  48433  lindslinindimp2lem2  48435  lindslinindimp2lem4  48437  lindslinindsimp2lem5  48438  lindslinindsimp2  48439  lincresunit1  48453  lincresunit2  48454  lincresunit3lem2  48456  lincresunit3  48457