Theorem difexd 5275

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439   ∖ cdif 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-in 3907  df-ss 3917

This theorem is referenced by:  sexp2  8088  sexp3  8095  ralxpmap  8836  domdifsn  8990  domunsncan  9007  mapdom2  9078  acni  9957  infdif  10120  infpss  10128  enfin1ai  10296  fpwwe2  10556  canthp1lem1  10565  hashf1lem1  14380  mrieqv2d  17564  mreexexlemd  17569  dpjidcl  19991  pnrmopn  23289  cmpfi  23354  csdfil  23840  ufileu  23865  filufint  23866  alexsublem  23990  bcth3  25289  iunmbl  25512  tdeglem4  26023  fdifsupp  32743  gsummptres2  33115  tocycfv  33170  cyc3conja  33218  rprmdvdsprod  33594  extvfvvcl  33679  extvfvcl  33680  esummono  34190  esumpad  34191  esumpad2  34192  insiga  34273  selvcllemh  42860  selvcllem4  42861  selvcllem5  42862  selvcl  42863  selvval2  42864  selvvvval  42865  selvadd  42868  selvmul  42869  fsuppssind  42873  tfsconcatun  43616  oaun2  43660  oaun3  43661  clcnvlem  43901  dssmapfv3d  44297  dssmapnvod  44298  ovolsplit  46269  intsal  46611  sge0ss  46693  sge0fodjrnlem  46697  iundjiun  46741  meaiunlelem  46749  iscnrm3rlem7  49228