Theorem difexd 5327

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3463   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5295

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3421  df-v 3465  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  sexp2  8150  sexp3  8157  ralxpmap  8915  domdifsn  9082  domunsncan  9100  mapdom2  9176  acni  10079  infdif  10241  infpss  10249  enfin1ai  10416  fpwwe2  10675  canthp1lem1  10684  hashf1lem1  14466  mrieqv2d  17645  mreexexlemd  17650  dpjidcl  20052  pnrmopn  23333  cmpfi  23398  csdfil  23884  ufileu  23909  filufint  23910  alexsublem  24034  bcth3  25345  iunmbl  25568  tdeglem4  26081  gsummptres2  32923  tocycfv  32989  cyc3conja  33037  rprmdvdsprod  33413  esummono  33898  esumpad  33899  esumpad2  33900  insiga  33981  selvcllemh  42268  selvcllem4  42269  selvcllem5  42270  selvcl  42271  selvval2  42272  selvvvval  42273  selvadd  42276  selvmul  42277  fsuppssind  42281  tfsconcatun  43038  oaun2  43082  oaun3  43083  clcnvlem  43325  dssmapfv3d  43721  dssmapnvod  43722  ovolsplit  45643  intsal  45985  sge0ss  46067  sge0fodjrnlem  46071  iundjiun  46115  meaiunlelem  46123  iscnrm3rlem7  48314