Theorem difexd 5286

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ∖ cdif 3911

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 5251

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 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931

This theorem is referenced by:  sexp2  8125  sexp3  8132  ralxpmap  8869  domdifsn  9024  domunsncan  9041  mapdom2  9112  acni  9998  infdif  10161  infpss  10169  enfin1ai  10337  fpwwe2  10596  canthp1lem1  10605  hashf1lem1  14420  mrieqv2d  17600  mreexexlemd  17605  dpjidcl  19990  pnrmopn  23230  cmpfi  23295  csdfil  23781  ufileu  23806  filufint  23807  alexsublem  23931  bcth3  25231  iunmbl  25454  tdeglem4  25965  fdifsupp  32608  gsummptres2  32993  tocycfv  33066  cyc3conja  33114  rprmdvdsprod  33505  esummono  34044  esumpad  34045  esumpad2  34046  insiga  34127  selvcllemh  42568  selvcllem4  42569  selvcllem5  42570  selvcl  42571  selvval2  42572  selvvvval  42573  selvadd  42576  selvmul  42577  fsuppssind  42581  tfsconcatun  43326  oaun2  43370  oaun3  43371  clcnvlem  43612  dssmapfv3d  44008  dssmapnvod  44009  ovolsplit  45986  intsal  46328  sge0ss  46410  sge0fodjrnlem  46414  iundjiun  46458  meaiunlelem  46466  iscnrm3rlem7  48934