Theorem difexd 5292

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-in 3905  df-ss 3915

This theorem is used by:  sexp2  8141  sexp3  8148  ralxpmap  8902  domdifsn  9057  domunsncan  9074  mapdom2  9145  acni  10095  infdif  10257  infpss  10265  enfin1ai  10433  fpwwe2  10699  canthp1lem1  10708  hashf1lem1  14567  mrieqv2d  17774  mreexexlemd  17779  dpjidcl  20235  isdrng3lem2  20967  selvcllemh  22407  selvcllem4  22408  selvcllem5  22409  selvcl  22410  selvval2  22411  selvvvval  22412  selvadd  22413  selvmul  22414  pnrmopn  23622  cmpfi  23687  csdfil  24174  ufileu  24199  filufint  24200  alexsublem  24324  bcth3  25613  iunmbl  25835  tdeglem4  26339  fdifsupp  33211  gsummptres2  33547  tocycfv  33603  cyc3conja  33651  dflring4  33963  rprmdvdsprod  33999  selvascl  34082  selvply1rhmlem2  34086  selvply1rhmlem4  34088  selvply1rhm  34090  selvply1rhm0  34091  extvfvcl  34101  esummono  34619  esumpad  34620  esumpad2  34621  insiga  34703  fsuppssind  43543  tfsconcatun  44282  oaun2  44326  oaun3  44327  clcnvlem  44567  dssmapfv3d  44963  dssmapnvod  44964  ovolsplit  46920  intsal  47262  sge0ss  47344  sge0fodjrnlem  47348  iundjiun  47392  meaiunlelem  47400  iscnrm3rlem7  49976