Theorem difexi 5301

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-in 3912  df-ss 3922

This theorem is referenced by:  oev  8495  naddcllem  8658  sbthlem2  9072  findcard  9144  findcard2  9145  pssnn  9149  ssfi  9153  frfi  9241  unfilem3  9263  marypha1lem  9389  wemapso  9509  inf3lem3  9595  dfac9  10116  dfacacn  10121  kmlem11  10140  kmlem12  10141  fin23lem28  10319  isf32lem6  10337  isf32lem7  10338  isf32lem8  10339  domtriomlem  10421  axdc2lem  10427  axcclem  10436  zornn0g  10484  konigthlem  10548  grothprim  10814  hashbclem  14485  fi1uzind  14540  brfi1uzind  14541  brfi1indALT  14543  opfi1uzind  14544  ramub1lem1  17081  pltfval  18380  isirred  20497  isdrng3lem1  20851  cntzsdrg  20905  subdrgint  20906  lssset  21054  xrs1mnd  21590  xrs10  21591  xrs1cmn  21592  xrge0subm  21593  xrge0cmn  21594  cnmsgngrp  21729  psgninv  21732  psdmul  22329  neitr  23337  lecldbas  23376  imasdsf1olem  24530  xrge0gsumle  24991  xrge0tsms  24992  i1fd  25840  lhop1lem  26172  reefgim  26613  cxpcn2  26911  logbmpt  26953  newval  28028  newf  28031  addsval  28155  mulsval  28302  nnsex  28511  tgplnfn  29057  plngval  29059  isplng  29060  axlowdimlem15  29306  axlowdim  29311  elntg  29334  uhgrspan1lem1  29650  upgrres1lem1  29659  nbgrval  29686  nbfusgrlevtxm1  29727  cusgrfilem3  29807  vtxdginducedm1lem1  29889  vtxdginducedm1fi  29894  finsumvtxdg2ssteplem4  29898  padct  33063  rprmval  33806  dimkerim  34017  onvf1odlem2  35588  satfv1lem  35854  satfdm  35861  satffunlem1lem2  35895  satffunlem2lem2  35898  nmulprop  36682  watvalN  40767  hvmapfval  42533  prjspval  43335  setindtr  43751  ssdifcl  44297  sssymdifcl  44298  clsk3nimkb  44766  iundjiunlem  47173  meaiuninclem  47194  meaiininclem  47200  lines  49511