Theorem difexg 5205

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

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3398   ∖ cdif 3850   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870

This theorem is referenced by:  difexi  5206  difexd  5207  difex2  7523  elpwun  7532  2oconcl  8208  fnoe  8215  difsnen  8705  sucdom2  8733  fodomr  8775  domss2  8783  domssex2  8784  domssex  8785  limenpsi  8799  brwdom2  9167  infeq5i  9229  infdifsn  9250  dfac8clem  9611  ssfin4  9889  isf34lem1  9951  compssiso  9953  fin1a2lem7  9985  fin1a2lem13  9991  fpwwe2lem12  10221  hashgt23el  13956  hashf1lem1OLD  13986  pmtrfv  18798  isirred  19671  isdrng2  19731  drngmcl  19734  drngid2  19737  isdrngd  19746  subdrgint  19801  cnmsubglem  20380  islindf4  20754  smadiadetlem1a  21514  basdif0  21804  tgdif0  21843  clsval2  21901  cmpcld  22253  ptcmplem2  22904  iunmbl  24404  tdeglem4OLD  24912  logbfval  25627  nbfusgrlevtxm2  27420  vtxdginducedm1  27585  frgrwopreglem1  28349  eigvecval  29931  elpwdifcl  30548  disjdifprg  30587  padct  30728  resf1o  30739  xrge00  30968  xrge0tsmsd  30990  tocycf  31057  ist0cld  31451  locfinref  31459  ldsysgenld  31794  sigapildsys  31796  carsgclctun  31954  sitgclg  31975  ballotlemfrc  32159  ballotlem8  32169  bnj852  32568  bnj865  32570  subfacp1lem5  32813  iscvm  32888  cvmsval  32895  mdvval  33133  topdifinffinlem  35204  pibt2  35274  poimirlem15  35478  voliunnfl  35507  fdc  35589  isdrngo2  35802  lzenom  40236  diophin  40238  diophren  40279  deg1mhm  40676  stoweidlem57  43216  fourierdlem102  43367  fourierdlem114  43379  pwsal  43474  gsumge0cl  43527  caragendifcl  43670  carageniuncllem1  43677  isomenndlem  43686  hoidmv1lelem2  43748  lincdifsn  45381  lindslinindsimp1  45414  lindslinindimp2lem2  45416  lindslinindimp2lem4  45418  lindslinindsimp2lem5  45419  lindslinindsimp2  45420  lincresunit1  45434  lincresunit2  45435  lincresunit3lem2  45437  lincresunit3  45438