Theorem difexd 5331

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ∖ cdif 3948

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 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968

This theorem is referenced by:  sexp2  8171  sexp3  8178  ralxpmap  8936  domdifsn  9094  domunsncan  9112  mapdom2  9188  acni  10085  infdif  10248  infpss  10256  enfin1ai  10424  fpwwe2  10683  canthp1lem1  10692  hashf1lem1  14494  mrieqv2d  17682  mreexexlemd  17687  dpjidcl  20078  pnrmopn  23351  cmpfi  23416  csdfil  23902  ufileu  23927  filufint  23928  alexsublem  24052  bcth3  25365  iunmbl  25588  tdeglem4  26099  fdifsupp  32694  gsummptres2  33056  tocycfv  33129  cyc3conja  33177  rprmdvdsprod  33562  esummono  34055  esumpad  34056  esumpad2  34057  insiga  34138  selvcllemh  42590  selvcllem4  42591  selvcllem5  42592  selvcl  42593  selvval2  42594  selvvvval  42595  selvadd  42598  selvmul  42599  fsuppssind  42603  tfsconcatun  43350  oaun2  43394  oaun3  43395  clcnvlem  43636  dssmapfv3d  44032  dssmapnvod  44033  ovolsplit  46003  intsal  46345  sge0ss  46427  sge0fodjrnlem  46431  iundjiun  46475  meaiunlelem  46483  iscnrm3rlem7  48843