Theorem difexi 5266

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-in 3904  df-ss 3914

This theorem is referenced by:  oev  8429  naddcllem  8591  sbthlem2  9001  findcard  9073  findcard2  9074  pssnn  9078  ssfi  9082  frfi  9169  unfilem3  9191  marypha1lem  9317  wemapso  9437  inf3lem3  9520  dfac9  10028  dfacacn  10033  kmlem11  10052  kmlem12  10053  fin23lem28  10231  isf32lem6  10249  isf32lem7  10250  isf32lem8  10251  domtriomlem  10333  axdc2lem  10339  axcclem  10348  zornn0g  10396  konigthlem  10459  grothprim  10725  hashbclem  14359  fi1uzind  14414  brfi1uzind  14415  brfi1indALT  14417  opfi1uzind  14418  ramub1lem1  16938  pltfval  18235  isirred  20337  cntzsdrg  20717  subdrgint  20718  lssset  20866  xrs1mnd  21377  xrs10  21378  xrs1cmn  21379  xrge0subm  21380  xrge0cmn  21381  cnmsgngrp  21516  psgninv  21519  psdmul  22081  neitr  23095  lecldbas  23134  imasdsf1olem  24288  xrge0gsumle  24749  xrge0tsms  24750  i1fd  25609  lhop1lem  25945  reefgim  26387  cxpcn2  26683  logbmpt  26725  newval  27796  newf  27799  addsval  27905  mulsval  28048  nnsex  28247  axlowdimlem15  28934  axlowdim  28939  elntg  28962  uhgrspan1lem1  29278  upgrres1lem1  29287  nbgrval  29314  nbfusgrlevtxm1  29355  cusgrfilem3  29436  vtxdginducedm1lem1  29518  vtxdginducedm1fi  29523  finsumvtxdg2ssteplem4  29527  rprmval  33481  dimkerim  33640  onvf1odlem2  35148  satfv1lem  35406  satfdm  35413  satffunlem1lem2  35447  satffunlem2lem2  35450  watvalN  40091  hvmapfval  41857  prjspval  42695  setindtr  43116  ssdifcl  43663  sssymdifcl  43664  clsk3nimkb  44132  iundjiunlem  46556  meaiuninclem  46577  meaiininclem  46583  lines  48831