Theorem difexi 5272

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922

This theorem is referenced by:  oev  8439  naddcllem  8601  sbthlem2  9012  findcard  9087  findcard2  9088  pssnn  9092  ssfi  9097  frfi  9190  unfilem3  9214  marypha1lem  9342  wemapso  9462  inf3lem3  9545  dfac9  10050  dfacacn  10055  kmlem11  10074  kmlem12  10075  fin23lem28  10253  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  domtriomlem  10355  axdc2lem  10361  axcclem  10370  zornn0g  10418  konigthlem  10481  grothprim  10747  hashbclem  14378  fi1uzind  14433  brfi1uzind  14434  brfi1indALT  14436  opfi1uzind  14437  ramub1lem1  16957  pltfval  18254  isirred  20323  cntzsdrg  20706  subdrgint  20707  lssset  20855  xrs1mnd  21366  xrs10  21367  xrs1cmn  21368  xrge0subm  21369  xrge0cmn  21370  cnmsgngrp  21505  psgninv  21508  psdmul  22070  neitr  23084  lecldbas  23123  imasdsf1olem  24278  xrge0gsumle  24739  xrge0tsms  24740  i1fd  25599  lhop1lem  25935  reefgim  26377  cxpcn2  26673  logbmpt  26715  newval  27784  newf  27787  addsval  27893  mulsval  28036  nnsex  28235  axlowdimlem15  28920  axlowdim  28925  elntg  28948  uhgrspan1lem1  29264  upgrres1lem1  29273  nbgrval  29300  nbfusgrlevtxm1  29341  cusgrfilem3  29422  vtxdginducedm1lem1  29504  vtxdginducedm1fi  29509  finsumvtxdg2ssteplem4  29513  rprmval  33472  dimkerim  33613  onvf1odlem2  35096  satfv1lem  35354  satfdm  35361  satffunlem1lem2  35395  satffunlem2lem2  35398  watvalN  39992  hvmapfval  41758  prjspval  42596  setindtr  43017  ssdifcl  43564  sssymdifcl  43565  clsk3nimkb  44033  iundjiunlem  46460  meaiuninclem  46481  meaiininclem  46487  lines  48736