Theorem difexd 5222

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3408   ∖ cdif 3863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-in 3873  df-ss 3883

This theorem is referenced by:  ralxpmap  8577  domdifsn  8728  domunsncan  8745  mapdom2  8817  acni  9659  infdif  9823  infpss  9831  enfin1ai  9998  fpwwe2  10257  canthp1lem1  10266  hashf1lem1  14020  mrieqv2d  17142  mreexexlemd  17147  dpjidcl  19445  pnrmopn  22240  cmpfi  22305  csdfil  22791  ufileu  22816  filufint  22817  alexsublem  22941  bcth3  24228  iunmbl  24450  tdeglem4  24957  gsummptres2  31032  tocycfv  31095  cyc3conja  31143  esummono  31734  esumpad  31735  esumpad2  31736  insiga  31817  sexp2  33530  sexp3  33536  selvval2lemn  39940  selvval2lem4  39941  selvval2lem5  39942  selvcl  39943  fsuppssind  39992  clcnvlem  40907  dssmapfv3d  41304  dssmapnvod  41305  ovolsplit  43204  intsal  43544  sge0ss  43625  sge0fodjrnlem  43629  iundjiun  43673  meaiunlelem  43681  iscnrm3rlem7  45913