Theorem difexg 5088

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

Syntax hints:   → wi 4   ∈ wcel 2050  Vcvv 3415   ∖ cdif 3828   ⊆ wss 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-dif 3834  df-in 3838  df-ss 3845

This theorem is referenced by:  difexi  5089  difex2  7301  elpwun  7310  2oconcl  7932  fnoe  7939  ralxpmap  8260  difsnen  8397  domdifsn  8398  domunsncan  8415  fodomr  8466  domss2  8474  domssex2  8475  domssex  8476  mapdom2  8486  limenpsi  8490  sucdom2  8511  brwdom2  8834  infeq5i  8895  infdifsn  8916  dfac8clem  9254  acni  9267  infdif  9431  infpss  9439  ssfin4  9532  isf34lem1  9594  compssiso  9596  enfin1ai  9606  fin1a2lem7  9628  fin1a2lem13  9634  fpwwe2lem13  9864  fpwwe2  9865  canthp1lem1  9874  hashgt23el  13601  hashf1lem1  13629  brfi1indALT  13672  mrieqv2d  16771  mreexexlemd  16776  pmtrfv  18344  dpjidcl  18933  isirred  19175  isdrng2  19238  drngmcl  19241  drngid2  19244  isdrngd  19253  subdrgint  19307  cnmsubglem  20313  islindf4  20687  smadiadetlem1a  20979  basdif0  21268  tgdif0  21307  clsval2  21365  pnrmopn  21658  cmpcld  21717  cmpfi  21723  csdfil  22209  ufileu  22234  filufint  22235  alexsublem  22359  ptcmplem2  22368  bcth3  23640  iunmbl  23860  tdeglem4  24360  logbfval  25072  nbfusgrlevtxm2  26866  vtxdginducedm1  27031  frgrwopreglem1  27849  eigvecval  29457  elpwdifcl  30064  disjdifprg  30094  padct  30210  resf1o  30221  xrge00  30405  tocycval  30446  xrge0tsmsd  30530  locfinref  30749  esummono  30957  esumpad  30958  esumpad2  30959  insiga  31041  ldsysgenld  31064  sigapildsys  31066  carsgclctun  31224  sitgclg  31245  ballotlemfrc  31430  ballotlem8  31440  bnj852  31840  bnj865  31842  subfacp1lem5  32016  iscvm  32091  cvmsval  32098  mdvval  32271  topdifinffinlem  34070  pibt2  34139  poimirlem15  34348  voliunnfl  34377  fdc  34462  isdrngo2  34678  lzenom  38762  diophin  38765  diophren  38806  deg1mhm  39203  sssymdifcl  39293  clcnvlem  39346  dssmapfv3d  39728  dssmapnvod  39729  ovolsplit  41705  stoweidlem57  41774  fourierdlem102  41925  fourierdlem114  41937  pwsal  42032  intsal  42045  gsumge0cl  42085  sge0ss  42126  sge0fodjrnlem  42130  iundjiunlem  42173  iundjiun  42174  meaiunlelem  42182  caragendifcl  42228  carageniuncllem1  42235  isomenndlem  42244  hoidmv1lelem2  42306  lincdifsn  43847  lindslinindsimp1  43880  lindslinindimp2lem2  43882  lindslinindimp2lem4  43884  lindslinindsimp2lem5  43885  lindslinindsimp2  43886  lincresunit1  43900  lincresunit2  43901  lincresunit3lem2  43903  lincresunit3  43904