Theorem difexg 5329

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ∖ cdif 3948   ⊆ wss 3951

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 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968

This theorem is referenced by:  difexi  5330  difexd  5331  difex2  7780  elpwun  7789  2oconcl  8541  fnoe  8548  difsnen  9093  sucdom2OLD  9122  fodomr  9168  domss2  9176  domssex2  9177  domssex  9178  limenpsi  9192  dif1enlem  9196  sucdom2  9243  brwdom2  9613  infeq5i  9676  infdifsn  9697  dfac8clem  10072  ssfin4  10350  isf34lem1  10412  compssiso  10414  fin1a2lem7  10446  fin1a2lem13  10452  fpwwe2lem12  10682  hashgt23el  14463  pmtrfv  19470  isirred  20419  isdrng2  20743  drngmclOLD  20751  drngid2  20752  isdrngd  20765  isdrngdOLD  20767  subdrgint  20804  cnmsubglem  21448  islindf4  21858  smadiadetlem1a  22669  basdif0  22960  tgdif0  22999  clsval2  23058  cmpcld  23410  ptcmplem2  24061  iunmbl  25588  logbfval  26833  nbfusgrlevtxm2  29395  vtxdginducedm1  29561  frgrwopreglem1  30331  eigvecval  31915  elpwdifcl  32545  disjdifprg  32588  mptiffisupp  32702  padct  32731  resf1o  32741  xrge00  33017  xrge0tsmsd  33065  tocycf  33137  ist0cld  33832  locfinref  33840  ldsysgenld  34161  sigapildsys  34163  carsgclctun  34323  sitgclg  34344  ballotlemfrc  34529  ballotlem8  34539  bnj852  34935  bnj865  34937  subfacp1lem5  35189  iscvm  35264  cvmsval  35271  mdvval  35509  topdifinffinlem  37348  pibt2  37418  poimirlem15  37642  voliunnfl  37671  fdc  37752  isdrngo2  37965  lzenom  42781  diophin  42783  diophren  42824  deg1mhm  43212  stoweidlem57  46072  fourierdlem102  46223  fourierdlem114  46235  pwsal  46330  gsumge0cl  46386  caragendifcl  46529  carageniuncllem1  46536  isomenndlem  46545  hoidmv1lelem2  46607  lincdifsn  48341  lindslinindsimp1  48374  lindslinindimp2lem2  48376  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  lincresunit1  48394  lincresunit2  48395  lincresunit3lem2  48397  lincresunit3  48398