Theorem difexd 5261

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3427   ∖ cdif 3882

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-in 3892  df-ss 3902

This theorem is referenced by:  sexp2  8085  sexp3  8092  ralxpmap  8833  domdifsn  8987  domunsncan  9004  mapdom2  9075  acni  9956  infdif  10119  infpss  10127  enfin1ai  10295  fpwwe2  10555  canthp1lem1  10564  hashf1lem1  14406  mrieqv2d  17594  mreexexlemd  17599  dpjidcl  20024  pnrmopn  23296  cmpfi  23361  csdfil  23847  ufileu  23872  filufint  23873  alexsublem  23997  bcth3  25286  iunmbl  25508  tdeglem4  26013  fdifsupp  32746  gsummptres2  33102  tocycfv  33158  cyc3conja  33206  rprmdvdsprod  33582  extvfvvcl  33667  extvfvcl  33668  esummono  34186  esumpad  34187  esumpad2  34188  insiga  34269  selvcllemh  43001  selvcllem4  43002  selvcllem5  43003  selvcl  43004  selvval2  43005  selvvvval  43006  selvadd  43009  selvmul  43010  fsuppssind  43014  tfsconcatun  43753  oaun2  43797  oaun3  43798  clcnvlem  44038  dssmapfv3d  44434  dssmapnvod  44435  ovolsplit  46404  intsal  46746  sge0ss  46828  sge0fodjrnlem  46832  iundjiun  46876  meaiunlelem  46884  iscnrm3rlem7  49409