Theorem difexg 5290

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091

This theorem is used by:  difexi  5291  difexd  5292  difex2  7775  elpwun  7784  2oconcl  8515  fnoe  8522  difsnen  9082  fodomr  9151  domss2  9159  domssex2  9160  domssex  9161  limenpsi  9175  dif1enlem  9179  sucdom2  9222  brwdom2  9571  infeq5i  9641  infdifsn  9662  dfac8clem  10115  ssfin4  10392  isf34lem1  10454  compssiso  10456  fin1a2lem7  10488  fin1a2lem13  10494  fpwwe2lem12  10731  hashgt23el  14573  pmtrfv  19672  isirred  20655  isdrng2  21003  drngid2  21016  isdrngd  21028  isdrngdOLD  21030  subdrgint  21066  cnmsubglem  21742  islindf4  22150  smadiadetlem1a  22984  basdif0  23277  tgdif0  23316  clsval2  23374  cmpcld  23726  ptcmplem2  24378  iunmbl  25880  logbfval  27124  nbfusgrlevtxm2  29965  vtxdginducedm1  30130  frgrwopreglem1  30919  eigvecval  32504  elpwdifcl  33170  disjdifprg  33217  mptiffisupp  33334  resf1o  33369  xrge00  33622  xrge0tsmsd  33681  tocycf  33725  ist0cld  34512  locfinref  34520  ldsysgenld  34840  sigapildsys  34842  carsgclctun  35000  sitgclg  35021  ballotlemfrc  35206  ballotlem8  35216  bnj852  35598  bnj865  35600  subfacp1lem5  36036  iscvm  36111  cvmsval  36118  mdvval  36356  ttcwf2  37406  topdifinffinlem  38364  pibt2  38434  poimirlem15  38647  voliunnfl  38676  fdc  38773  isdrngo2  38986  lzenom  43875  diophin  43877  diophren  43914  deg1mhm  44296  stoweidlem57  47161  fourierdlem102  47312  fourierdlem114  47324  pwsal  47419  gsumge0cl  47475  caragendifcl  47618  carageniuncllem1  47625  isomenndlem  47634  hoidmv1lelem2  47696  lincdifsn  49630  lindslinindsimp1  49663  lindslinindimp2lem2  49665  lindslinindimp2lem4  49667  lindslinindsimp2lem5  49668  lindslinindsimp2  49669  lincresunit1  49683  lincresunit2  49684  lincresunit3lem2  49686  lincresunit3  49687