Theorem difexg 5246

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  difexi  5247  difexd  5248  difex2  7588  elpwun  7597  2oconcl  8295  fnoe  8302  difsnen  8794  sucdom2  8822  fodomr  8864  domss2  8872  domssex2  8873  domssex  8874  limenpsi  8888  brwdom2  9262  infeq5i  9324  infdifsn  9345  dfac8clem  9719  ssfin4  9997  isf34lem1  10059  compssiso  10061  fin1a2lem7  10093  fin1a2lem13  10099  fpwwe2lem12  10329  hashgt23el  14067  hashf1lem1OLD  14097  pmtrfv  18975  isirred  19856  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  subdrgint  19986  cnmsubglem  20573  islindf4  20955  smadiadetlem1a  21720  basdif0  22011  tgdif0  22050  clsval2  22109  cmpcld  22461  ptcmplem2  23112  iunmbl  24622  tdeglem4OLD  25130  logbfval  25845  nbfusgrlevtxm2  27648  vtxdginducedm1  27813  frgrwopreglem1  28577  eigvecval  30159  elpwdifcl  30776  disjdifprg  30815  padct  30956  resf1o  30967  xrge00  31197  xrge0tsmsd  31219  tocycf  31286  ist0cld  31685  locfinref  31693  ldsysgenld  32028  sigapildsys  32030  carsgclctun  32188  sitgclg  32209  ballotlemfrc  32393  ballotlem8  32403  bnj852  32801  bnj865  32803  subfacp1lem5  33046  iscvm  33121  cvmsval  33128  mdvval  33366  topdifinffinlem  35445  pibt2  35515  poimirlem15  35719  voliunnfl  35748  fdc  35830  isdrngo2  36043  lzenom  40508  diophin  40510  diophren  40551  deg1mhm  40948  stoweidlem57  43488  fourierdlem102  43639  fourierdlem114  43651  pwsal  43746  gsumge0cl  43799  caragendifcl  43942  carageniuncllem1  43949  isomenndlem  43958  hoidmv1lelem2  44020  lincdifsn  45653  lindslinindsimp1  45686  lindslinindimp2lem2  45688  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  lincresunit1  45706  lincresunit2  45707  lincresunit3lem2  45709  lincresunit3  45710