Theorem difexd 5291

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446   ∖ cdif 3910

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-in 3920  df-ss 3930

This theorem is referenced by:  sexp2  8083  sexp3  8090  ralxpmap  8841  domdifsn  9005  domunsncan  9023  mapdom2  9099  acni  9990  infdif  10154  infpss  10162  enfin1ai  10329  fpwwe2  10588  canthp1lem1  10597  hashf1lem1  14365  mrieqv2d  17533  mreexexlemd  17538  dpjidcl  19851  pnrmopn  22731  cmpfi  22796  csdfil  23282  ufileu  23307  filufint  23308  alexsublem  23432  bcth3  24732  iunmbl  24954  tdeglem4  25461  gsummptres2  31965  tocycfv  32028  cyc3conja  32076  esummono  32742  esumpad  32743  esumpad2  32744  insiga  32825  selvcllemh  40816  selvcllem4  40817  selvcllem5  40818  selvcl  40819  selvval2  40820  selvadd  40821  selvmul  40822  fsuppssind  40826  tfsconcatun  41730  oaun2  41774  oaun3  41775  clcnvlem  42017  dssmapfv3d  42413  dssmapnvod  42414  ovolsplit  44349  intsal  44691  sge0ss  44773  sge0fodjrnlem  44777  iundjiun  44821  meaiunlelem  44829  iscnrm3rlem7  47099