Theorem difexi 5327

Description: Existence of a difference, inference version of difexg 5326. (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 5326	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  oev  8509  naddcllem  8671  sbthlem2  9080  findcard  9159  findcard2  9160  pssnn  9164  ssfi  9169  phplem2OLD  9214  phpOLD  9218  pssnnOLD  9261  findcard2OLD  9280  frfi  9284  unfilem3  9308  marypha1lem  9424  wemapso  9542  inf3lem3  9621  dfac9  10127  dfacacn  10132  kmlem11  10151  kmlem12  10152  fin23lem28  10331  isf32lem6  10349  isf32lem7  10350  isf32lem8  10351  domtriomlem  10433  axdc2lem  10439  axcclem  10448  zornn0g  10496  konigthlem  10559  grothprim  10825  hashbclem  14407  fi1uzind  14454  brfi1uzind  14455  brfi1indALT  14457  opfi1uzind  14458  ramub1lem1  16955  pltfval  18280  isirred  20222  cntzsdrg  20406  subdrgint  20407  lssset  20532  xrs1mnd  20968  xrs10  20969  xrs1cmn  20970  xrge0subm  20971  xrge0cmn  20972  cnmsgngrp  21116  psgninv  21119  neitr  22666  lecldbas  22705  imasdsf1olem  23861  xrge0gsumle  24331  xrge0tsms  24332  i1fd  25180  lhop1lem  25512  reefgim  25944  cxpcn2  26234  logbmpt  26273  newval  27330  newf  27333  addsval  27426  mulsval  27545  axlowdimlem15  28194  axlowdim  28199  elntg  28222  uhgrspan1lem1  28537  upgrres1lem1  28546  nbgrval  28573  nbfusgrlevtxm1  28614  cusgrfilem3  28694  vtxdginducedm1lem1  28776  vtxdginducedm1fi  28781  finsumvtxdg2ssteplem4  28785  rprmval  32585  dimkerim  32657  satfv1lem  34291  satfdm  34298  satffunlem1lem2  34332  satffunlem2lem2  34335  watvalN  38802  hvmapfval  40568  prjspval  41289  setindtr  41696  ssdifcl  42255  sssymdifcl  42256  clsk3nimkb  42724  iundjiunlem  45110  meaiuninclem  45131  meaiininclem  45137  lines  47319