Theorem difexd 5302

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-in 3918  df-ss 3928

This theorem is referenced by:  sexp2  8142  sexp3  8149  ralxpmap  8894  domdifsn  9048  domunsncan  9065  mapdom2  9136  acni  10029  infdif  10191  infpss  10199  enfin1ai  10368  fpwwe2  10628  canthp1lem1  10637  hashf1lem1  14492  mrieqv2d  17695  mreexexlemd  17700  dpjidcl  20130  selvcllemh  22257  selvcllem4  22258  selvcllem5  22259  selvcl  22260  selvval2  22261  selvvvval  22262  selvadd  22263  selvmul  22264  pnrmopn  23469  cmpfi  23534  csdfil  24020  ufileu  24045  filufint  24046  alexsublem  24170  bcth3  25459  iunmbl  25681  tdeglem4  26186  fdifsupp  32971  gsummptres2  33314  tocycfv  33370  cyc3conja  33418  dflring4  33733  rprmdvdsprod  33769  selvascl  33852  selvply1rhmlem2  33856  selvply1rhmlem4  33858  selvply1rhm  33860  selvply1rhm0  33861  extvfvvcl  33870  extvfvcl  33871  esummono  34389  esumpad  34390  esumpad2  34391  insiga  34472  fsuppssind  43252  tfsconcatun  43991  oaun2  44035  oaun3  44036  clcnvlem  44276  dssmapfv3d  44672  dssmapnvod  44673  ovolsplit  46629  intsal  46971  sge0ss  47053  sge0fodjrnlem  47057  iundjiun  47101  meaiunlelem  47109  iscnrm3rlem7  49644