Theorem difexd 5330

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  sexp2  8132  sexp3  8139  ralxpmap  8890  domdifsn  9054  domunsncan  9072  mapdom2  9148  acni  10040  infdif  10204  infpss  10212  enfin1ai  10379  fpwwe2  10638  canthp1lem1  10647  hashf1lem1  14415  mrieqv2d  17583  mreexexlemd  17588  dpjidcl  19928  pnrmopn  22847  cmpfi  22912  csdfil  23398  ufileu  23423  filufint  23424  alexsublem  23548  bcth3  24848  iunmbl  25070  tdeglem4  25577  gsummptres2  32236  tocycfv  32299  cyc3conja  32347  esummono  33083  esumpad  33084  esumpad2  33085  insiga  33166  selvcllemh  41200  selvcllem4  41201  selvcllem5  41202  selvcl  41203  selvval2  41204  selvvvval  41205  selvadd  41208  selvmul  41209  fsuppssind  41213  tfsconcatun  42135  oaun2  42179  oaun3  42180  clcnvlem  42422  dssmapfv3d  42818  dssmapnvod  42819  ovolsplit  44752  intsal  45094  sge0ss  45176  sge0fodjrnlem  45180  iundjiun  45224  meaiunlelem  45232  iscnrm3rlem7  47627