Theorem difexi 5267

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ∖ cdif 3887

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 5231

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 3391  df-v 3432  df-dif 3893  df-in 3897  df-ss 3907

This theorem is referenced by:  oev  8442  naddcllem  8605  sbthlem2  9019  findcard  9091  findcard2  9092  pssnn  9096  ssfi  9100  frfi  9188  unfilem3  9210  marypha1lem  9339  wemapso  9459  inf3lem3  9542  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  10482  grothprim  10748  hashbclem  14405  fi1uzind  14460  brfi1uzind  14461  brfi1indALT  14463  opfi1uzind  14464  ramub1lem1  16988  pltfval  18286  isirred  20390  cntzsdrg  20770  subdrgint  20771  lssset  20919  xrs1mnd  21430  xrs10  21431  xrs1cmn  21432  xrge0subm  21433  xrge0cmn  21434  cnmsgngrp  21569  psgninv  21572  psdmul  22142  neitr  23155  lecldbas  23194  imasdsf1olem  24348  xrge0gsumle  24809  xrge0tsms  24810  i1fd  25658  lhop1lem  25990  reefgim  26428  cxpcn2  26723  logbmpt  26765  newval  27841  newf  27844  addsval  27968  mulsval  28115  nnsex  28324  axlowdimlem15  29039  axlowdim  29044  elntg  29067  uhgrspan1lem1  29383  upgrres1lem1  29392  nbgrval  29419  nbfusgrlevtxm1  29460  cusgrfilem3  29541  vtxdginducedm1lem1  29623  vtxdginducedm1fi  29628  finsumvtxdg2ssteplem4  29632  padct  32806  rprmval  33591  dimkerim  33787  onvf1odlem2  35302  satfv1lem  35560  satfdm  35567  satffunlem1lem2  35601  satffunlem2lem2  35604  watvalN  40453  hvmapfval  42219  prjspval  43050  setindtr  43470  ssdifcl  44016  sssymdifcl  44017  clsk3nimkb  44485  iundjiunlem  46905  meaiuninclem  46926  meaiininclem  46932  lines  49219