Theorem difexd 5253

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432   ∖ cdif 3884

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  ralxpmap  8684  domdifsn  8841  domunsncan  8859  mapdom2  8935  acni  9801  infdif  9965  infpss  9973  enfin1ai  10140  fpwwe2  10399  canthp1lem1  10408  hashf1lem1  14168  mrieqv2d  17348  mreexexlemd  17353  dpjidcl  19661  pnrmopn  22494  cmpfi  22559  csdfil  23045  ufileu  23070  filufint  23071  alexsublem  23195  bcth3  24495  iunmbl  24717  tdeglem4  25224  gsummptres2  31313  tocycfv  31376  cyc3conja  31424  esummono  32022  esumpad  32023  esumpad2  32024  insiga  32105  sexp2  33793  sexp3  33799  selvval2lemn  40227  selvval2lem4  40228  selvval2lem5  40229  selvcl  40230  fsuppssind  40282  clcnvlem  41231  dssmapfv3d  41627  dssmapnvod  41628  ovolsplit  43529  intsal  43869  sge0ss  43950  sge0fodjrnlem  43954  iundjiun  43998  meaiunlelem  44006  iscnrm3rlem7  46240