Theorem difexi 5330

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∖ cdif 3948

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968

This theorem is referenced by:  oev  8552  naddcllem  8714  sbthlem2  9124  findcard  9203  findcard2  9204  pssnn  9208  ssfi  9213  phplem2OLD  9255  phpOLD  9259  frfi  9321  unfilem3  9345  marypha1lem  9473  wemapso  9591  inf3lem3  9670  dfac9  10177  dfacacn  10182  kmlem11  10201  kmlem12  10202  fin23lem28  10380  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  domtriomlem  10482  axdc2lem  10488  axcclem  10497  zornn0g  10545  konigthlem  10608  grothprim  10874  hashbclem  14491  fi1uzind  14546  brfi1uzind  14547  brfi1indALT  14549  opfi1uzind  14550  ramub1lem1  17064  pltfval  18376  isirred  20419  cntzsdrg  20803  subdrgint  20804  lssset  20931  xrs1mnd  21422  xrs10  21423  xrs1cmn  21424  xrge0subm  21425  xrge0cmn  21426  cnmsgngrp  21597  psgninv  21600  psdmul  22170  neitr  23188  lecldbas  23227  imasdsf1olem  24383  xrge0gsumle  24855  xrge0tsms  24856  i1fd  25716  lhop1lem  26052  reefgim  26494  cxpcn2  26789  logbmpt  26831  newval  27894  newf  27897  addsval  27995  mulsval  28135  nnsex  28323  axlowdimlem15  28971  axlowdim  28976  elntg  28999  uhgrspan1lem1  29317  upgrres1lem1  29326  nbgrval  29353  nbfusgrlevtxm1  29394  cusgrfilem3  29475  vtxdginducedm1lem1  29557  vtxdginducedm1fi  29562  finsumvtxdg2ssteplem4  29566  rprmval  33544  dimkerim  33678  satfv1lem  35367  satfdm  35374  satffunlem1lem2  35408  satffunlem2lem2  35411  watvalN  39995  hvmapfval  41761  prjspval  42613  setindtr  43036  ssdifcl  43584  sssymdifcl  43585  clsk3nimkb  44053  iundjiunlem  46474  meaiuninclem  46495  meaiininclem  46501  lines  48652