Theorem difexd 5280

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ∖ cdif 3900

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 2709  ax-sep 5245

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920

This theorem is referenced by:  sexp2  8100  sexp3  8107  ralxpmap  8848  domdifsn  9002  domunsncan  9019  mapdom2  9090  acni  9969  infdif  10132  infpss  10140  enfin1ai  10308  fpwwe2  10568  canthp1lem1  10577  hashf1lem1  14392  mrieqv2d  17576  mreexexlemd  17581  dpjidcl  20006  pnrmopn  23304  cmpfi  23369  csdfil  23855  ufileu  23880  filufint  23881  alexsublem  24005  bcth3  25304  iunmbl  25527  tdeglem4  26038  fdifsupp  32781  gsummptres2  33153  tocycfv  33209  cyc3conja  33257  rprmdvdsprod  33633  extvfvvcl  33718  extvfvcl  33719  esummono  34238  esumpad  34239  esumpad2  34240  insiga  34321  selvcllemh  42967  selvcllem4  42968  selvcllem5  42969  selvcl  42970  selvval2  42971  selvvvval  42972  selvadd  42975  selvmul  42976  fsuppssind  42980  tfsconcatun  43723  oaun2  43767  oaun3  43768  clcnvlem  44008  dssmapfv3d  44404  dssmapnvod  44405  ovolsplit  46375  intsal  46717  sge0ss  46799  sge0fodjrnlem  46803  iundjiun  46847  meaiunlelem  46855  iscnrm3rlem7  49334