Theorem difexi 5280

Description: Existence of a difference, inference version of difexg 5279. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)

Hypothesis

Ref	Expression
difexi.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
difexi	⊢ (𝐴 ∖ 𝐵) ∈ V

Proof of Theorem difexi

Step	Hyp	Ref	Expression
1		difexi.1	. 2 ⊢ 𝐴 ∈ V
2		difexg 5279	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928

This theorem is referenced by:  oev  8455  naddcllem  8617  sbthlem2  9029  findcard  9104  findcard2  9105  pssnn  9109  ssfi  9114  frfi  9208  unfilem3  9232  marypha1lem  9360  wemapso  9480  inf3lem3  9559  dfac9  10066  dfacacn  10071  kmlem11  10090  kmlem12  10091  fin23lem28  10269  isf32lem6  10287  isf32lem7  10288  isf32lem8  10289  domtriomlem  10371  axdc2lem  10377  axcclem  10386  zornn0g  10434  konigthlem  10497  grothprim  10763  hashbclem  14393  fi1uzind  14448  brfi1uzind  14449  brfi1indALT  14451  opfi1uzind  14452  ramub1lem1  16973  pltfval  18266  isirred  20304  cntzsdrg  20687  subdrgint  20688  lssset  20815  xrs1mnd  21297  xrs10  21298  xrs1cmn  21299  xrge0subm  21300  xrge0cmn  21301  cnmsgngrp  21464  psgninv  21467  psdmul  22029  neitr  23043  lecldbas  23082  imasdsf1olem  24237  xrge0gsumle  24698  xrge0tsms  24699  i1fd  25558  lhop1lem  25894  reefgim  26336  cxpcn2  26632  logbmpt  26674  newval  27739  newf  27742  addsval  27845  mulsval  27988  nnsex  28187  axlowdimlem15  28859  axlowdim  28864  elntg  28887  uhgrspan1lem1  29203  upgrres1lem1  29212  nbgrval  29239  nbfusgrlevtxm1  29280  cusgrfilem3  29361  vtxdginducedm1lem1  29443  vtxdginducedm1fi  29448  finsumvtxdg2ssteplem4  29452  rprmval  33460  dimkerim  33596  onvf1odlem2  35064  satfv1lem  35322  satfdm  35329  satffunlem1lem2  35363  satffunlem2lem2  35366  watvalN  39960  hvmapfval  41726  prjspval  42564  setindtr  42986  ssdifcl  43533  sssymdifcl  43534  clsk3nimkb  44002  iundjiunlem  46430  meaiuninclem  46451  meaiininclem  46457  lines  48693