Theorem difexi 5329

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3946

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 5300

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 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  oev  8514  naddcllem  8675  sbthlem2  9084  findcard  9163  findcard2  9164  pssnn  9168  ssfi  9173  phplem2OLD  9218  phpOLD  9222  pssnnOLD  9265  findcard2OLD  9284  frfi  9288  unfilem3  9312  marypha1lem  9428  wemapso  9546  inf3lem3  9625  dfac9  10131  dfacacn  10136  kmlem11  10155  kmlem12  10156  fin23lem28  10335  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  domtriomlem  10437  axdc2lem  10443  axcclem  10452  zornn0g  10500  konigthlem  10563  grothprim  10829  hashbclem  14411  fi1uzind  14458  brfi1uzind  14459  brfi1indALT  14461  opfi1uzind  14462  ramub1lem1  16959  pltfval  18284  isirred  20233  cntzsdrg  20418  subdrgint  20419  lssset  20544  xrs1mnd  20983  xrs10  20984  xrs1cmn  20985  xrge0subm  20986  xrge0cmn  20987  cnmsgngrp  21132  psgninv  21135  neitr  22684  lecldbas  22723  imasdsf1olem  23879  xrge0gsumle  24349  xrge0tsms  24350  i1fd  25198  lhop1lem  25530  reefgim  25962  cxpcn2  26254  logbmpt  26293  newval  27350  newf  27353  addsval  27446  mulsval  27565  axlowdimlem15  28214  axlowdim  28219  elntg  28242  uhgrspan1lem1  28557  upgrres1lem1  28566  nbgrval  28593  nbfusgrlevtxm1  28634  cusgrfilem3  28714  vtxdginducedm1lem1  28796  vtxdginducedm1fi  28801  finsumvtxdg2ssteplem4  28805  rprmval  32633  dimkerim  32712  satfv1lem  34353  satfdm  34360  satffunlem1lem2  34394  satffunlem2lem2  34397  watvalN  38864  hvmapfval  40630  prjspval  41345  setindtr  41763  ssdifcl  42322  sssymdifcl  42323  clsk3nimkb  42791  iundjiunlem  45175  meaiuninclem  45196  meaiininclem  45202  lines  47417