Theorem difexi 5277

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920

This theorem is referenced by:  oev  8451  naddcllem  8614  sbthlem2  9028  findcard  9100  findcard2  9101  pssnn  9105  ssfi  9109  frfi  9197  unfilem3  9219  marypha1lem  9348  wemapso  9468  inf3lem3  9551  dfac9  10059  dfacacn  10064  kmlem11  10083  kmlem12  10084  fin23lem28  10262  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  domtriomlem  10364  axdc2lem  10370  axcclem  10379  zornn0g  10427  konigthlem  10491  grothprim  10757  hashbclem  14387  fi1uzind  14442  brfi1uzind  14443  brfi1indALT  14445  opfi1uzind  14446  ramub1lem1  16966  pltfval  18264  isirred  20367  cntzsdrg  20747  subdrgint  20748  lssset  20896  xrs1mnd  21407  xrs10  21408  xrs1cmn  21409  xrge0subm  21410  xrge0cmn  21411  cnmsgngrp  21546  psgninv  21549  psdmul  22121  neitr  23136  lecldbas  23175  imasdsf1olem  24329  xrge0gsumle  24790  xrge0tsms  24791  i1fd  25650  lhop1lem  25986  reefgim  26428  cxpcn2  26724  logbmpt  26766  newval  27843  newf  27846  addsval  27970  mulsval  28117  nnsex  28326  axlowdimlem15  29041  axlowdim  29046  elntg  29069  uhgrspan1lem1  29385  upgrres1lem1  29394  nbgrval  29421  nbfusgrlevtxm1  29462  cusgrfilem3  29543  vtxdginducedm1lem1  29625  vtxdginducedm1fi  29630  finsumvtxdg2ssteplem4  29634  rprmval  33609  dimkerim  33805  onvf1odlem2  35320  satfv1lem  35578  satfdm  35585  satffunlem1lem2  35619  satffunlem2lem2  35622  watvalN  40369  hvmapfval  42135  prjspval  42961  setindtr  43381  ssdifcl  43927  sssymdifcl  43928  clsk3nimkb  44396  iundjiunlem  46817  meaiuninclem  46838  meaiininclem  46844  lines  49091