Theorem difexd 5262

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-in 3892  df-ss 3902

This theorem is referenced by:  sexp2  8090  sexp3  8097  ralxpmap  8838  domdifsn  8992  domunsncan  9009  mapdom2  9080  acni  9962  infdif  10125  infpss  10133  enfin1ai  10301  fpwwe2  10561  canthp1lem1  10570  hashf1lem1  14412  mrieqv2d  17600  mreexexlemd  17605  dpjidcl  20030  selvcllemh  22117  selvcllem4  22118  selvcllem5  22119  selvcl  22120  selvval2  22121  selvvvval  22122  selvadd  22123  selvmul  22124  pnrmopn  23330  cmpfi  23395  csdfil  23881  ufileu  23906  filufint  23907  alexsublem  24031  bcth3  25320  iunmbl  25542  tdeglem4  26047  fdifsupp  32781  gsummptres2  33138  tocycfv  33194  cyc3conja  33242  dflring4  33593  rprmdvdsprod  33629  selvascl  33713  selvply1rhmlem2  33717  selvply1rhmlem4  33719  selvply1rhm  33721  selvply1rhm0  33722  extvfvvcl  33731  extvfvcl  33732  esummono  34250  esumpad  34251  esumpad2  34252  insiga  34333  fsuppssind  43058  tfsconcatun  43797  oaun2  43841  oaun3  43842  clcnvlem  44082  dssmapfv3d  44478  dssmapnvod  44479  ovolsplit  46445  intsal  46787  sge0ss  46869  sge0fodjrnlem  46873  iundjiun  46917  meaiunlelem  46925  iscnrm3rlem7  49450