Theorem difexd 5329

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ∖ cdif 3945

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 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  sexp2  8134  sexp3  8141  ralxpmap  8892  domdifsn  9056  domunsncan  9074  mapdom2  9150  acni  10042  infdif  10206  infpss  10214  enfin1ai  10381  fpwwe2  10640  canthp1lem1  10649  hashf1lem1  14419  mrieqv2d  17587  mreexexlemd  17592  dpjidcl  19969  pnrmopn  23067  cmpfi  23132  csdfil  23618  ufileu  23643  filufint  23644  alexsublem  23768  bcth3  25072  iunmbl  25294  tdeglem4  25801  gsummptres2  32463  tocycfv  32526  cyc3conja  32574  esummono  33338  esumpad  33339  esumpad2  33340  insiga  33421  selvcllemh  41454  selvcllem4  41455  selvcllem5  41456  selvcl  41457  selvval2  41458  selvvvval  41459  selvadd  41462  selvmul  41463  fsuppssind  41467  tfsconcatun  42389  oaun2  42433  oaun3  42434  clcnvlem  42676  dssmapfv3d  43072  dssmapnvod  43073  ovolsplit  45003  intsal  45345  sge0ss  45427  sge0fodjrnlem  45431  iundjiun  45475  meaiunlelem  45483  iscnrm3rlem7  47667