Theorem difexd 5301

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454   ∖ cdif 3901

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-in 3911  df-ss 3921

This theorem is used by:  sexp2  8140  sexp3  8147  ralxpmap  8892  domdifsn  9046  domunsncan  9063  mapdom2  9134  acni  10036  infdif  10198  infpss  10206  enfin1ai  10374  fpwwe2  10634  canthp1lem1  10643  hashf1lem1  14499  mrieqv2d  17701  mreexexlemd  17706  dpjidcl  20136  isdrng3lem2  20863  selvcllemh  22299  selvcllem4  22300  selvcllem5  22301  selvcl  22302  selvval2  22303  selvvvval  22304  selvadd  22305  selvmul  22306  pnrmopn  23511  cmpfi  23576  csdfil  24062  ufileu  24087  filufint  24088  alexsublem  24212  bcth3  25501  iunmbl  25723  tdeglem4  26228  fdifsupp  33041  gsummptres2  33382  tocycfv  33438  cyc3conja  33486  dflring4  33797  rprmdvdsprod  33833  selvascl  33916  selvply1rhmlem2  33920  selvply1rhmlem4  33922  selvply1rhm  33924  selvply1rhm0  33925  extvfvvcl  33934  extvfvcl  33935  esummono  34453  esumpad  34454  esumpad2  34455  insiga  34536  fsuppssind  43353  tfsconcatun  44092  oaun2  44136  oaun3  44137  clcnvlem  44377  dssmapfv3d  44773  dssmapnvod  44774  ovolsplit  46730  intsal  47072  sge0ss  47154  sge0fodjrnlem  47158  iundjiun  47202  meaiunlelem  47210  iscnrm3rlem7  49752