Theorem difexg 5016

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

Syntax hints:   → wi 4   ∈ wcel 2157  Vcvv 3402   ∖ cdif 3777   ⊆ wss 3780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-in 3787  df-ss 3794

This theorem is referenced by:  difexi  5017  difex2  7209  elpwun  7217  2oconcl  7830  fnoe  7837  ralxpmap  8154  difsnen  8291  domdifsn  8292  domunsncan  8309  fodomr  8360  domss2  8368  domssex2  8369  domssex  8370  mapdom2  8380  limenpsi  8384  sucdom2  8405  findcard  8448  findcard2  8449  frfi  8454  unfilem3  8475  brwdom2  8727  infeq5i  8790  infdifsn  8811  dfac8clem  9148  acni  9161  dfac9  9253  dfacacn  9258  infpss  9334  ssfin4  9427  fin23lem28  9457  isf32lem6  9475  isf32lem7  9476  isf32lem8  9477  isf34lem1  9489  compssiso  9491  enfin1ai  9501  fin1a2lem7  9523  fin1a2lem13  9529  axdc2lem  9565  axcclem  9574  zornn0g  9622  fpwwe2lem13  9759  fpwwe2  9760  canthp1lem1  9769  grothprim  9951  hashbclem  13473  hashf1lem1  13476  fi1uzind  13516  brfi1uzind  13517  brfi1indALT  13519  ramub1lem1  15967  mrieqv2d  16524  mreexexlemd  16529  pltfval  17184  pmtrfv  18093  dpjidcl  18679  isirred  18921  isdrng2  18981  drngmcl  18984  drngid2  18987  isdrngd  18996  lssset  19158  xrs1mnd  20012  xrs1cmn  20014  xrge0subm  20015  cnmsubglem  20037  islindf4  20408  smadiadetlem1a  20702  basdif0  20992  tgdif0  21031  clsval2  21089  neitr  21219  lecldbas  21258  pnrmopn  21382  cmpcld  21440  cmpfi  21446  csdfil  21932  ufileu  21957  filufint  21958  alexsublem  22082  ptcmplem2  22091  xrge0gsumle  22870  xrge0tsms  22871  bcth3  23362  iunmbl  23557  i1fd  23685  tdeglem4  24057  reefgim  24441  logbmpt  24763  logbfval  24765  axlowdimlem15  26073  axlowdim  26078  elntg  26101  nbfusgrlevtxm2  26519  cusgrfilem3  26604  vtxdginducedm1  26690  frgrwopreglem1  27510  eigvecval  29106  elpwdifcl  29706  disjdifprg  29736  padct  29847  resf1o  29855  xrge00  30034  xrge0tsmsd  30133  locfinref  30256  esummono  30464  esumpad  30465  esumpad2  30466  insiga  30548  ldsysgenld  30571  sigapildsys  30573  carsgclctun  30731  sitgclg  30752  ballotlemfrc  30936  ballotlem8  30946  bnj852  31336  bnj865  31338  subfacp1lem5  31511  iscvm  31586  cvmsval  31593  mdvval  31746  topdifinffinlem  33530  poimirlem15  33756  voliunnfl  33785  fdc  33871  isdrngo2  34087  watvalN  35792  hvmapfval  37558  lzenom  37853  diophin  37856  diophren  37897  cntzsdrg  38291  deg1mhm  38304  sssymdifcl  38395  clcnvlem  38448  dssmapfv3d  38831  dssmapnvod  38832  ovolsplit  40702  stoweidlem57  40771  fourierdlem102  40922  fourierdlem114  40934  pwsal  41032  intsal  41045  gsumge0cl  41085  sge0ss  41126  sge0fodjrnlem  41130  iundjiunlem  41173  iundjiun  41174  meaiunlelem  41182  caragendifcl  41228  carageniuncllem1  41235  isomenndlem  41244  hoidmv1lelem2  41306  lincdifsn  42799  lindslinindsimp1  42832  lindslinindimp2lem2  42834  lindslinindimp2lem4  42836  lindslinindsimp2lem5  42837  lindslinindsimp2  42838  lincresunit1  42852  lincresunit2  42853  lincresunit3lem2  42855  lincresunit3  42856