Theorem difexd 5289

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-in 3913  df-ss 3923

This theorem is referenced by:  sexp2  8128  sexp3  8135  ralxpmap  8880  domdifsn  9034  domunsncan  9051  mapdom2  9122  acni  10003  infdif  10166  infpss  10174  enfin1ai  10343  fpwwe2  10603  canthp1lem1  10612  hashf1lem1  14470  mrieqv2d  17673  mreexexlemd  17678  dpjidcl  20102  selvcllemh  22192  selvcllem4  22193  selvcllem5  22194  selvcl  22195  selvval2  22196  selvvvval  22197  selvadd  22198  selvmul  22199  pnrmopn  23405  cmpfi  23470  csdfil  23956  ufileu  23981  filufint  23982  alexsublem  24106  bcth3  25395  iunmbl  25617  tdeglem4  26122  fdifsupp  32889  gsummptres2  33235  tocycfv  33291  cyc3conja  33339  dflring4  33696  rprmdvdsprod  33732  selvascl  33816  selvply1rhmlem2  33820  selvply1rhmlem4  33822  selvply1rhm  33824  selvply1rhm0  33825  extvfvvcl  33834  extvfvcl  33835  esummono  34353  esumpad  34354  esumpad2  34355  insiga  34436  fsuppssind  43180  tfsconcatun  43919  oaun2  43963  oaun3  43964  clcnvlem  44204  dssmapfv3d  44600  dssmapnvod  44601  ovolsplit  46567  intsal  46909  sge0ss  46991  sge0fodjrnlem  46995  iundjiun  47039  meaiunlelem  47047  iscnrm3rlem7  49572