Theorem difexd 5301

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-ss 3943

This theorem is referenced by:  sexp2  8145  sexp3  8152  ralxpmap  8910  domdifsn  9068  domunsncan  9086  mapdom2  9162  acni  10059  infdif  10222  infpss  10230  enfin1ai  10398  fpwwe2  10657  canthp1lem1  10666  hashf1lem1  14473  mrieqv2d  17651  mreexexlemd  17656  dpjidcl  20041  pnrmopn  23281  cmpfi  23346  csdfil  23832  ufileu  23857  filufint  23858  alexsublem  23982  bcth3  25283  iunmbl  25506  tdeglem4  26017  fdifsupp  32662  gsummptres2  33047  tocycfv  33120  cyc3conja  33168  rprmdvdsprod  33549  esummono  34085  esumpad  34086  esumpad2  34087  insiga  34168  selvcllemh  42603  selvcllem4  42604  selvcllem5  42605  selvcl  42606  selvval2  42607  selvvvval  42608  selvadd  42611  selvmul  42612  fsuppssind  42616  tfsconcatun  43361  oaun2  43405  oaun3  43406  clcnvlem  43647  dssmapfv3d  44043  dssmapnvod  44044  ovolsplit  46017  intsal  46359  sge0ss  46441  sge0fodjrnlem  46445  iundjiun  46489  meaiunlelem  46497  iscnrm3rlem7  48920