Theorem difexi 5252

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432   ∖ cdif 3884

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  oev  8344  sbthlem2  8871  findcard  8946  findcard2  8947  pssnn  8951  ssfi  8956  phplem2OLD  9001  phpOLD  9005  pssnnOLD  9040  findcard2OLD  9056  frfi  9059  unfilem3  9080  marypha1lem  9192  wemapso  9310  inf3lem3  9388  dfac9  9892  dfacacn  9897  kmlem11  9916  kmlem12  9917  fin23lem28  10096  isf32lem6  10114  isf32lem7  10115  isf32lem8  10116  domtriomlem  10198  axdc2lem  10204  axcclem  10213  zornn0g  10261  konigthlem  10324  grothprim  10590  hashbclem  14164  fi1uzind  14211  brfi1uzind  14212  brfi1indALT  14214  opfi1uzind  14215  ramub1lem1  16727  pltfval  18049  isirred  19941  cntzsdrg  20070  subdrgint  20071  lssset  20195  xrs1mnd  20636  xrs10  20637  xrs1cmn  20638  xrge0subm  20639  xrge0cmn  20640  cnmsgngrp  20784  psgninv  20787  neitr  22331  lecldbas  22370  imasdsf1olem  23526  xrge0gsumle  23996  xrge0tsms  23997  i1fd  24845  lhop1lem  25177  reefgim  25609  cxpcn2  25899  logbmpt  25938  axlowdimlem15  27324  axlowdim  27329  elntg  27352  uhgrspan1lem1  27667  upgrres1lem1  27676  nbgrval  27703  nbfusgrlevtxm1  27744  cusgrfilem3  27824  vtxdginducedm1lem1  27906  vtxdginducedm1fi  27911  finsumvtxdg2ssteplem4  27915  rprmval  31664  dimkerim  31708  satfv1lem  33324  satfdm  33331  satffunlem1lem2  33365  satffunlem2lem2  33368  naddcllem  33831  newval  34039  newf  34042  addsval  34126  watvalN  38007  hvmapfval  39773  prjspval  40442  setindtr  40846  ssdifcl  41178  sssymdifcl  41179  clsk3nimkb  41650  iundjiunlem  43997  meaiuninclem  44018  meaiininclem  44024  lines  46077