Theorem difexg 5302

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457   ∖ cdif 3903   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-in 3913  df-ss 3923

This theorem is used by:  difexi  5303  difexd  5304  difex2  7761  elpwun  7770  2oconcl  8490  fnoe  8497  difsnen  9050  fodomr  9119  domss2  9127  domssex2  9128  domssex  9129  limenpsi  9143  dif1enlem  9147  sucdom2  9190  brwdom2  9538  infeq5i  9608  infdifsn  9629  dfac8clem  10028  ssfin4  10305  isf34lem1  10367  compssiso  10369  fin1a2lem7  10401  fin1a2lem13  10407  fpwwe2lem12  10638  hashgt23el  14474  pmtrfv  19545  isirred  20526  isdrng2  20872  drngid2  20885  isdrngd  20897  isdrngdOLD  20899  subdrgint  20935  cnmsubglem  21609  islindf4  22017  smadiadetlem1a  22849  basdif0  23139  tgdif0  23178  clsval2  23236  cmpcld  23588  ptcmplem2  24239  iunmbl  25741  logbfval  26984  nbfusgrlevtxm2  29757  vtxdginducedm1  29922  frgrwopreglem1  30692  eigvecval  32277  elpwdifcl  32901  disjdifprg  32949  mptiffisupp  33067  resf1o  33104  xrge00  33357  xrge0tsmsd  33416  tocycf  33460  ist0cld  34246  locfinref  34254  ldsysgenld  34574  sigapildsys  34576  carsgclctun  34735  sitgclg  34756  ballotlemfrc  34941  ballotlem8  34951  bnj852  35333  bnj865  35335  subfacp1lem5  35689  iscvm  35764  cvmsval  35771  mdvval  36009  ttcwf2  37069  topdifinffinlem  38026  pibt2  38096  poimirlem15  38319  voliunnfl  38348  fdc  38429  isdrngo2  38642  lzenom  43534  diophin  43536  diophren  43573  deg1mhm  43960  stoweidlem57  46804  fourierdlem102  46955  fourierdlem114  46967  pwsal  47062  gsumge0cl  47118  caragendifcl  47261  carageniuncllem1  47268  isomenndlem  47277  hoidmv1lelem2  47339  lincdifsn  49237  lindslinindsimp1  49270  lindslinindimp2lem2  49272  lindslinindimp2lem4  49274  lindslinindsimp2lem5  49275  lindslinindsimp2  49276  lincresunit1  49290  lincresunit2  49291  lincresunit3lem2  49293  lincresunit3  49294