Theorem difexd 5289

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3914

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934

This theorem is referenced by:  sexp2  8128  sexp3  8135  ralxpmap  8872  domdifsn  9028  domunsncan  9046  mapdom2  9118  acni  10005  infdif  10168  infpss  10176  enfin1ai  10344  fpwwe2  10603  canthp1lem1  10612  hashf1lem1  14427  mrieqv2d  17607  mreexexlemd  17612  dpjidcl  19997  pnrmopn  23237  cmpfi  23302  csdfil  23788  ufileu  23813  filufint  23814  alexsublem  23938  bcth3  25238  iunmbl  25461  tdeglem4  25972  fdifsupp  32615  gsummptres2  33000  tocycfv  33073  cyc3conja  33121  rprmdvdsprod  33512  esummono  34051  esumpad  34052  esumpad2  34053  insiga  34134  selvcllemh  42575  selvcllem4  42576  selvcllem5  42577  selvcl  42578  selvval2  42579  selvvvval  42580  selvadd  42583  selvmul  42584  fsuppssind  42588  tfsconcatun  43333  oaun2  43377  oaun3  43378  clcnvlem  43619  dssmapfv3d  44015  dssmapnvod  44016  ovolsplit  45993  intsal  46335  sge0ss  46417  sge0fodjrnlem  46421  iundjiun  46465  meaiunlelem  46473  iscnrm3rlem7  48938