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  32205  tocycfv  32268  cyc3conja  32316  esummono  33052  esumpad  33053  esumpad2  33054  insiga  33135  selvcllemh  41152  selvcllem4  41153  selvcllem5  41154  selvcl  41155  selvval2  41156  selvvvval  41157  selvadd  41160  selvmul  41161  fsuppssind  41165  tfsconcatun  42087  oaun2  42131  oaun3  42132  clcnvlem  42374  dssmapfv3d  42770  dssmapnvod  42771  ovolsplit  44704  intsal  45046  sge0ss  45128  sge0fodjrnlem  45132  iundjiun  45176  meaiunlelem  45184  iscnrm3rlem7  47579