Theorem difexd 5270

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-in 3910  df-ss 3920

This theorem is referenced by:  sexp2  8079  sexp3  8086  ralxpmap  8823  domdifsn  8977  domunsncan  8994  mapdom2  9065  acni  9939  infdif  10102  infpss  10110  enfin1ai  10278  fpwwe2  10537  canthp1lem1  10546  hashf1lem1  14362  mrieqv2d  17545  mreexexlemd  17550  dpjidcl  19939  pnrmopn  23228  cmpfi  23293  csdfil  23779  ufileu  23804  filufint  23805  alexsublem  23929  bcth3  25229  iunmbl  25452  tdeglem4  25963  fdifsupp  32635  gsummptres2  33015  tocycfv  33060  cyc3conja  33108  rprmdvdsprod  33480  esummono  34037  esumpad  34038  esumpad2  34039  insiga  34120  selvcllemh  42573  selvcllem4  42574  selvcllem5  42575  selvcl  42576  selvval2  42577  selvvvval  42578  selvadd  42581  selvmul  42582  fsuppssind  42586  tfsconcatun  43330  oaun2  43374  oaun3  43375  clcnvlem  43616  dssmapfv3d  44012  dssmapnvod  44013  ovolsplit  45989  intsal  46331  sge0ss  46413  sge0fodjrnlem  46417  iundjiun  46461  meaiunlelem  46469  iscnrm3rlem7  48950