Theorem difexi 5348

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993

This theorem is referenced by:  oev  8570  naddcllem  8732  sbthlem2  9150  findcard  9229  findcard2  9230  pssnn  9234  ssfi  9240  phplem2OLD  9281  phpOLD  9285  frfi  9349  unfilem3  9373  marypha1lem  9502  wemapso  9620  inf3lem3  9699  dfac9  10206  dfacacn  10211  kmlem11  10230  kmlem12  10231  fin23lem28  10409  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  domtriomlem  10511  axdc2lem  10517  axcclem  10526  zornn0g  10574  konigthlem  10637  grothprim  10903  hashbclem  14501  fi1uzind  14556  brfi1uzind  14557  brfi1indALT  14559  opfi1uzind  14560  ramub1lem1  17073  pltfval  18401  isirred  20445  cntzsdrg  20825  subdrgint  20826  lssset  20954  xrs1mnd  21445  xrs10  21446  xrs1cmn  21447  xrge0subm  21448  xrge0cmn  21449  cnmsgngrp  21620  psgninv  21623  psdmul  22193  neitr  23209  lecldbas  23248  imasdsf1olem  24404  xrge0gsumle  24874  xrge0tsms  24875  i1fd  25735  lhop1lem  26072  reefgim  26512  cxpcn2  26807  logbmpt  26849  newval  27912  newf  27915  addsval  28013  mulsval  28153  nnsex  28341  axlowdimlem15  28989  axlowdim  28994  elntg  29017  uhgrspan1lem1  29335  upgrres1lem1  29344  nbgrval  29371  nbfusgrlevtxm1  29412  cusgrfilem3  29493  vtxdginducedm1lem1  29575  vtxdginducedm1fi  29580  finsumvtxdg2ssteplem4  29584  rprmval  33509  dimkerim  33640  satfv1lem  35330  satfdm  35337  satffunlem1lem2  35371  satffunlem2lem2  35374  watvalN  39950  hvmapfval  41716  prjspval  42558  setindtr  42981  ssdifcl  43533  sssymdifcl  43534  clsk3nimkb  44002  iundjiunlem  46380  meaiuninclem  46401  meaiininclem  46407  lines  48465