Theorem difexd 5278

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 5276	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3442   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5248

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-dif 3905  df-in 3909  df-ss 3919

This theorem is referenced by:  ralxpmap  8760  domdifsn  8924  domunsncan  8942  mapdom2  9018  acni  9907  infdif  10071  infpss  10079  enfin1ai  10246  fpwwe2  10505  canthp1lem1  10514  hashf1lem1  14273  mrieqv2d  17446  mreexexlemd  17451  dpjidcl  19756  pnrmopn  22600  cmpfi  22665  csdfil  23151  ufileu  23176  filufint  23177  alexsublem  23301  bcth3  24601  iunmbl  24823  tdeglem4  25330  gsummptres2  31598  tocycfv  31661  cyc3conja  31709  esummono  32318  esumpad  32319  esumpad2  32320  insiga  32401  sexp2  34075  sexp3  34081  selvval2lemn  40530  selvval2lem4  40531  selvval2lem5  40532  selvcl  40533  fsuppssind  40591  clcnvlem  41602  dssmapfv3d  41998  dssmapnvod  41999  ovolsplit  43915  intsal  44255  sge0ss  44337  sge0fodjrnlem  44341  iundjiun  44385  meaiunlelem  44393  iscnrm3rlem7  46656