Theorem difexd 5300

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

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

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 2734  ax-sep 5255

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919

This theorem is used by:  sexp2  8147  sexp3  8154  ralxpmap  8906  domdifsn  9061  domunsncan  9078  mapdom2  9149  acni  10051  infdif  10213  infpss  10221  enfin1ai  10389  fpwwe2  10655  canthp1lem1  10664  hashf1lem1  14522  mrieqv2d  17731  mreexexlemd  17736  dpjidcl  20188  isdrng3lem2  20916  selvcllemh  22354  selvcllem4  22355  selvcllem5  22356  selvcl  22357  selvval2  22358  selvvvval  22359  selvadd  22360  selvmul  22361  pnrmopn  23569  cmpfi  23634  csdfil  24121  ufileu  24146  filufint  24147  alexsublem  24271  bcth3  25560  iunmbl  25782  tdeglem4  26287  fdifsupp  33144  gsummptres2  33480  tocycfv  33536  cyc3conja  33584  dflring4  33895  rprmdvdsprod  33931  selvascl  34014  selvply1rhmlem2  34018  selvply1rhmlem4  34020  selvply1rhm  34022  selvply1rhm0  34023  extvfvcl  34033  esummono  34551  esumpad  34552  esumpad2  34553  insiga  34635  fsuppssind  43426  tfsconcatun  44165  oaun2  44209  oaun3  44210  clcnvlem  44450  dssmapfv3d  44846  dssmapnvod  44847  ovolsplit  46803  intsal  47145  sge0ss  47227  sge0fodjrnlem  47231  iundjiun  47275  meaiunlelem  47283  iscnrm3rlem7  49859