Theorem difexg 5284

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ∖ cdif 3911   ⊆ wss 3914

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 2701  ax-sep 5251

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931

This theorem is referenced by:  difexi  5285  difexd  5286  difex2  7736  elpwun  7745  2oconcl  8467  fnoe  8474  difsnen  9023  fodomr  9092  domss2  9100  domssex2  9101  domssex  9102  limenpsi  9116  dif1enlem  9120  sucdom2  9167  brwdom2  9526  infeq5i  9589  infdifsn  9610  dfac8clem  9985  ssfin4  10263  isf34lem1  10325  compssiso  10327  fin1a2lem7  10359  fin1a2lem13  10365  fpwwe2lem12  10595  hashgt23el  14389  pmtrfv  19382  isirred  20328  isdrng2  20652  drngmclOLD  20660  drngid2  20661  isdrngd  20674  isdrngdOLD  20676  subdrgint  20712  cnmsubglem  21347  islindf4  21747  smadiadetlem1a  22550  basdif0  22840  tgdif0  22879  clsval2  22937  cmpcld  23289  ptcmplem2  23940  iunmbl  25454  logbfval  26700  nbfusgrlevtxm2  29305  vtxdginducedm1  29471  frgrwopreglem1  30241  eigvecval  31825  elpwdifcl  32455  disjdifprg  32504  mptiffisupp  32616  padct  32643  resf1o  32653  xrge00  32953  xrge0tsmsd  33002  tocycf  33074  ist0cld  33823  locfinref  33831  ldsysgenld  34150  sigapildsys  34152  carsgclctun  34312  sitgclg  34333  ballotlemfrc  34518  ballotlem8  34528  bnj852  34911  bnj865  34913  subfacp1lem5  35171  iscvm  35246  cvmsval  35253  mdvval  35491  topdifinffinlem  37335  pibt2  37405  poimirlem15  37629  voliunnfl  37658  fdc  37739  isdrngo2  37952  lzenom  42758  diophin  42760  diophren  42801  deg1mhm  43189  stoweidlem57  46055  fourierdlem102  46206  fourierdlem114  46218  pwsal  46313  gsumge0cl  46369  caragendifcl  46512  carageniuncllem1  46519  isomenndlem  46528  hoidmv1lelem2  46590  lincdifsn  48413  lindslinindsimp1  48446  lindslinindimp2lem2  48448  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lincresunit1  48466  lincresunit2  48467  lincresunit3lem2  48469  lincresunit3  48470