Theorem difexd 5296

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-in 3906  df-ss 3916

This theorem is used by:  sexp2  8145  sexp3  8152  ralxpmap  8906  domdifsn  9061  domunsncan  9078  mapdom2  9149  acni  10051  infdif  10213  infpss  10221  enfin1ai  10389  fpwwe2  10655  canthp1lem1  10664  hashf1lem1  14523  mrieqv2d  17730  mreexexlemd  17735  dpjidcl  20190  isdrng3lem2  20918  selvcllemh  22356  selvcllem4  22357  selvcllem5  22358  selvcl  22359  selvval2  22360  selvvvval  22361  selvadd  22362  selvmul  22363  pnrmopn  23571  cmpfi  23636  csdfil  24123  ufileu  24148  filufint  24149  alexsublem  24273  bcth3  25562  iunmbl  25784  tdeglem4  26288  fdifsupp  33160  gsummptres2  33496  tocycfv  33552  cyc3conja  33600  dflring4  33911  rprmdvdsprod  33947  selvascl  34030  selvply1rhmlem2  34034  selvply1rhmlem4  34036  selvply1rhm  34038  selvply1rhm0  34039  extvfvcl  34049  esummono  34567  esumpad  34568  esumpad2  34569  insiga  34651  fsuppssind  43442  tfsconcatun  44181  oaun2  44225  oaun3  44226  clcnvlem  44466  dssmapfv3d  44862  dssmapnvod  44863  ovolsplit  46819  intsal  47161  sge0ss  47243  sge0fodjrnlem  47247  iundjiun  47291  meaiunlelem  47299  iscnrm3rlem7  49875