Theorem difexg 5282

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919

This theorem is referenced by:  difexi  5283  difexd  5284  difex2  7738  elpwun  7747  2oconcl  8466  fnoe  8473  difsnen  9025  fodomr  9094  domss2  9102  domssex2  9103  domssex  9104  limenpsi  9118  dif1enlem  9122  sucdom2  9165  brwdom2  9515  infeq5i  9585  infdifsn  9606  dfac8clem  9982  ssfin4  10261  isf34lem1  10323  compssiso  10325  fin1a2lem7  10357  fin1a2lem13  10363  fpwwe2lem12  10594  hashgt23el  14431  pmtrfv  19483  isirred  20455  isdrng2  20780  drngmclOLD  20788  drngid2  20789  isdrngd  20802  isdrngdOLD  20804  subdrgint  20840  cnmsubglem  21470  islindf4  21878  smadiadetlem1a  22711  basdif0  23001  tgdif0  23040  clsval2  23098  cmpcld  23450  ptcmplem2  24101  iunmbl  25603  logbfval  26843  nbfusgrlevtxm2  29536  vtxdginducedm1  29701  frgrwopreglem1  30471  eigvecval  32056  elpwdifcl  32685  disjdifprg  32735  mptiffisupp  32856  resf1o  32893  xrge00  33153  xrge0tsmsd  33214  tocycf  33258  ist0cld  34091  locfinref  34099  ldsysgenld  34418  sigapildsys  34420  carsgclctun  34579  sitgclg  34600  ballotlemfrc  34785  ballotlem8  34795  bnj852  35177  bnj865  35179  subfacp1lem5  35495  iscvm  35570  cvmsval  35577  mdvval  35815  ttcwf2  36846  topdifinffinlem  37802  pibt2  37872  poimirlem15  38095  voliunnfl  38124  fdc  38205  isdrngo2  38418  lzenom  43312  diophin  43314  diophren  43351  deg1mhm  43738  stoweidlem57  46592  fourierdlem102  46743  fourierdlem114  46755  pwsal  46850  gsumge0cl  46906  caragendifcl  47049  carageniuncllem1  47056  isomenndlem  47065  hoidmv1lelem2  47127  lincdifsn  49007  lindslinindsimp1  49040  lindslinindimp2lem2  49042  lindslinindimp2lem4  49044  lindslinindsimp2lem5  49045  lindslinindsimp2  49046  lincresunit1  49060  lincresunit2  49061  lincresunit3lem2  49063  lincresunit3  49064