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  27351  newf  27354  addsval  27448  mulsval  27568  nnsex  27698  axlowdimlem15  28245  axlowdim  28250  elntg  28273  uhgrspan1lem1  28588  upgrres1lem1  28597  nbgrval  28624  nbfusgrlevtxm1  28665  cusgrfilem3  28745  vtxdginducedm1lem1  28827  vtxdginducedm1fi  28832  finsumvtxdg2ssteplem4  28836  rprmval  32664  dimkerim  32743  satfv1lem  34384  satfdm  34391  satffunlem1lem2  34425  satffunlem2lem2  34428  watvalN  38912  hvmapfval  40678  prjspval  41393  setindtr  41811  ssdifcl  42370  sssymdifcl  42371  clsk3nimkb  42839  iundjiunlem  45223  meaiuninclem  45244  meaiininclem  45250  lines  47465