Theorem difexd 5349

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993

This theorem is referenced by:  sexp2  8187  sexp3  8194  ralxpmap  8954  domdifsn  9120  domunsncan  9138  mapdom2  9214  acni  10114  infdif  10277  infpss  10285  enfin1ai  10453  fpwwe2  10712  canthp1lem1  10721  hashf1lem1  14504  mrieqv2d  17697  mreexexlemd  17702  dpjidcl  20102  pnrmopn  23372  cmpfi  23437  csdfil  23923  ufileu  23948  filufint  23949  alexsublem  24073  bcth3  25384  iunmbl  25607  tdeglem4  26119  gsummptres2  33036  tocycfv  33102  cyc3conja  33150  rprmdvdsprod  33527  esummono  34018  esumpad  34019  esumpad2  34020  insiga  34101  selvcllemh  42535  selvcllem4  42536  selvcllem5  42537  selvcl  42538  selvval2  42539  selvvvval  42540  selvadd  42543  selvmul  42544  fsuppssind  42548  tfsconcatun  43299  oaun2  43343  oaun3  43344  clcnvlem  43585  dssmapfv3d  43981  dssmapnvod  43982  ovolsplit  45909  intsal  46251  sge0ss  46333  sge0fodjrnlem  46337  iundjiun  46381  meaiunlelem  46389  iscnrm3rlem7  48626