Theorem difexd 5292

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091

This theorem is used by:  sexp2  8163  sexp3  8170  ralxpmap  8924  domdifsn  9079  domunsncan  9096  mapdom2  9167  acni  10124  infdif  10286  infpss  10294  enfin1ai  10462  fpwwe2  10728  canthp1lem1  10737  hashf1lem1  14600  mrieqv2d  17813  mreexexlemd  17818  dpjidcl  20274  isdrng3lem2  21006  selvcllemh  22446  selvcllem4  22447  selvcllem5  22448  selvcl  22449  selvval2  22450  selvvvval  22451  selvadd  22452  selvmul  22453  pnrmopn  23661  cmpfi  23726  csdfil  24213  ufileu  24238  filufint  24239  alexsublem  24363  bcth3  25652  iunmbl  25874  tdeglem4  26378  fdifsupp  33278  gsummptres2  33614  tocycfv  33670  cyc3conja  33718  dflring4  34030  rprmdvdsprod  34066  selvascl  34149  selvply1rhmlem2  34153  selvply1rhmlem4  34155  selvply1rhm  34157  selvply1rhm0  34158  extvfvcl  34168  esummono  34686  esumpad  34687  esumpad2  34688  insiga  34770  fsuppssind  43622  tfsconcatun  44339  oaun2  44383  oaun3  44384  clcnvlem  44623  dssmapfv3d  45019  dssmapnvod  45020  ovolsplit  46998  intsal  47340  sge0ss  47422  sge0fodjrnlem  47426  iundjiun  47470  meaiunlelem  47478  iscnrm3rlem7  50054