Theorem difexd 5269

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ∖ cdif 3887

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 5232

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 3391  df-v 3432  df-dif 3893  df-in 3897  df-ss 3907

This theorem is referenced by:  sexp2  8091  sexp3  8098  ralxpmap  8839  domdifsn  8993  domunsncan  9010  mapdom2  9081  acni  9962  infdif  10125  infpss  10133  enfin1ai  10301  fpwwe2  10561  canthp1lem1  10570  hashf1lem1  14412  mrieqv2d  17600  mreexexlemd  17605  dpjidcl  20030  pnrmopn  23322  cmpfi  23387  csdfil  23873  ufileu  23898  filufint  23899  alexsublem  24023  bcth3  25312  iunmbl  25534  tdeglem4  26039  fdifsupp  32777  gsummptres2  33133  tocycfv  33189  cyc3conja  33237  rprmdvdsprod  33613  extvfvvcl  33698  extvfvcl  33699  esummono  34218  esumpad  34219  esumpad2  34220  insiga  34301  selvcllemh  43033  selvcllem4  43034  selvcllem5  43035  selvcl  43036  selvval2  43037  selvvvval  43038  selvadd  43041  selvmul  43042  fsuppssind  43046  tfsconcatun  43789  oaun2  43833  oaun3  43834  clcnvlem  44074  dssmapfv3d  44470  dssmapnvod  44471  ovolsplit  46440  intsal  46782  sge0ss  46864  sge0fodjrnlem  46868  iundjiun  46912  meaiunlelem  46920  iscnrm3rlem7  49439