Theorem difexd 5281

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928

This theorem is referenced by:  sexp2  8102  sexp3  8109  ralxpmap  8846  domdifsn  9001  domunsncan  9018  mapdom2  9089  acni  9974  infdif  10137  infpss  10145  enfin1ai  10313  fpwwe2  10572  canthp1lem1  10581  hashf1lem1  14396  mrieqv2d  17580  mreexexlemd  17585  dpjidcl  19974  pnrmopn  23263  cmpfi  23328  csdfil  23814  ufileu  23839  filufint  23840  alexsublem  23964  bcth3  25264  iunmbl  25487  tdeglem4  25998  fdifsupp  32658  gsummptres2  33036  tocycfv  33081  cyc3conja  33129  rprmdvdsprod  33498  esummono  34037  esumpad  34038  esumpad2  34039  insiga  34120  selvcllemh  42561  selvcllem4  42562  selvcllem5  42563  selvcl  42564  selvval2  42565  selvvvval  42566  selvadd  42569  selvmul  42570  fsuppssind  42574  tfsconcatun  43319  oaun2  43363  oaun3  43364  clcnvlem  43605  dssmapfv3d  44001  dssmapnvod  44002  ovolsplit  45979  intsal  46321  sge0ss  46403  sge0fodjrnlem  46407  iundjiun  46451  meaiunlelem  46459  iscnrm3rlem7  48927