Theorem difexd 5277

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   ∖ 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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

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 3401  df-v 3443  df-dif 3905  df-in 3909  df-ss 3919

This theorem is referenced by:  sexp2  8090  sexp3  8097  ralxpmap  8838  domdifsn  8992  domunsncan  9009  mapdom2  9080  acni  9959  infdif  10122  infpss  10130  enfin1ai  10298  fpwwe2  10558  canthp1lem1  10567  hashf1lem1  14382  mrieqv2d  17566  mreexexlemd  17571  dpjidcl  19993  pnrmopn  23291  cmpfi  23356  csdfil  23842  ufileu  23867  filufint  23868  alexsublem  23992  bcth3  25291  iunmbl  25514  tdeglem4  26025  fdifsupp  32766  gsummptres2  33138  tocycfv  33193  cyc3conja  33241  rprmdvdsprod  33617  extvfvvcl  33702  extvfvcl  33703  esummono  34213  esumpad  34214  esumpad2  34215  insiga  34296  selvcllemh  42890  selvcllem4  42891  selvcllem5  42892  selvcl  42893  selvval2  42894  selvvvval  42895  selvadd  42898  selvmul  42899  fsuppssind  42903  tfsconcatun  43646  oaun2  43690  oaun3  43691  clcnvlem  43931  dssmapfv3d  44327  dssmapnvod  44328  ovolsplit  46299  intsal  46641  sge0ss  46723  sge0fodjrnlem  46727  iundjiun  46771  meaiunlelem  46779  iscnrm3rlem7  49258