Theorem difexd 5336

Description: Existence of a difference. (Contributed by SN, 16-Jul-2024.)

Hypothesis

Ref	Expression
difexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
difexd	⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)

Proof of Theorem difexd

Step	Hyp	Ref	Expression
1		difexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		difexg 5334	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979

This theorem is referenced by:  sexp2  8169  sexp3  8176  ralxpmap  8934  domdifsn  9092  domunsncan  9110  mapdom2  9186  acni  10082  infdif  10245  infpss  10253  enfin1ai  10421  fpwwe2  10680  canthp1lem1  10689  hashf1lem1  14490  mrieqv2d  17683  mreexexlemd  17688  dpjidcl  20092  pnrmopn  23366  cmpfi  23431  csdfil  23917  ufileu  23942  filufint  23943  alexsublem  24067  bcth3  25378  iunmbl  25601  tdeglem4  26113  fdifsupp  32699  gsummptres2  33038  tocycfv  33111  cyc3conja  33159  rprmdvdsprod  33541  esummono  34034  esumpad  34035  esumpad2  34036  insiga  34117  selvcllemh  42566  selvcllem4  42567  selvcllem5  42568  selvcl  42569  selvval2  42570  selvvvval  42571  selvadd  42574  selvmul  42575  fsuppssind  42579  tfsconcatun  43326  oaun2  43370  oaun3  43371  clcnvlem  43612  dssmapfv3d  44008  dssmapnvod  44009  ovolsplit  45943  intsal  46285  sge0ss  46367  sge0fodjrnlem  46371  iundjiun  46415  meaiunlelem  46423  iscnrm3rlem7  48742