Theorem difexi 5300

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923

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 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-ss 3943

This theorem is referenced by:  oev  8524  naddcllem  8686  sbthlem2  9096  findcard  9175  findcard2  9176  pssnn  9180  ssfi  9185  phplem2OLD  9227  phpOLD  9229  frfi  9291  unfilem3  9315  marypha1lem  9443  wemapso  9563  inf3lem3  9642  dfac9  10149  dfacacn  10154  kmlem11  10173  kmlem12  10174  fin23lem28  10352  isf32lem6  10370  isf32lem7  10371  isf32lem8  10372  domtriomlem  10454  axdc2lem  10460  axcclem  10469  zornn0g  10517  konigthlem  10580  grothprim  10846  hashbclem  14468  fi1uzind  14523  brfi1uzind  14524  brfi1indALT  14526  opfi1uzind  14527  ramub1lem1  17044  pltfval  18339  isirred  20377  cntzsdrg  20760  subdrgint  20761  lssset  20888  xrs1mnd  21370  xrs10  21371  xrs1cmn  21372  xrge0subm  21373  xrge0cmn  21374  cnmsgngrp  21537  psgninv  21540  psdmul  22102  neitr  23116  lecldbas  23155  imasdsf1olem  24310  xrge0gsumle  24771  xrge0tsms  24772  i1fd  25632  lhop1lem  25968  reefgim  26410  cxpcn2  26706  logbmpt  26748  newval  27811  newf  27814  addsval  27912  mulsval  28052  nnsex  28240  axlowdimlem15  28881  axlowdim  28886  elntg  28909  uhgrspan1lem1  29225  upgrres1lem1  29234  nbgrval  29261  nbfusgrlevtxm1  29302  cusgrfilem3  29383  vtxdginducedm1lem1  29465  vtxdginducedm1fi  29470  finsumvtxdg2ssteplem4  29474  rprmval  33477  dimkerim  33613  satfv1lem  35330  satfdm  35337  satffunlem1lem2  35371  satffunlem2lem2  35374  watvalN  39958  hvmapfval  41724  prjspval  42573  setindtr  42995  ssdifcl  43542  sssymdifcl  43543  clsk3nimkb  44011  iundjiunlem  46436  meaiuninclem  46457  meaiininclem  46463  lines  48659