Theorem difexd 5248

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  ralxpmap  8642  domdifsn  8795  domunsncan  8812  mapdom2  8884  acni  9732  infdif  9896  infpss  9904  enfin1ai  10071  fpwwe2  10330  canthp1lem1  10339  hashf1lem1  14096  mrieqv2d  17265  mreexexlemd  17270  dpjidcl  19576  pnrmopn  22402  cmpfi  22467  csdfil  22953  ufileu  22978  filufint  22979  alexsublem  23103  bcth3  24400  iunmbl  24622  tdeglem4  25129  gsummptres2  31215  tocycfv  31278  cyc3conja  31326  esummono  31922  esumpad  31923  esumpad2  31924  insiga  32005  sexp2  33720  sexp3  33726  selvval2lemn  40153  selvval2lem4  40154  selvval2lem5  40155  selvcl  40156  fsuppssind  40205  clcnvlem  41120  dssmapfv3d  41516  dssmapnvod  41517  ovolsplit  43419  intsal  43759  sge0ss  43840  sge0fodjrnlem  43844  iundjiun  43888  meaiunlelem  43896  iscnrm3rlem7  46128