Theorem difexi 5261

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

Syntax hints:   ∈ wcel 2121  Vcvv 3433   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-in 3892  df-ss 3902

This theorem is referenced by:  oev  8443  naddcllem  8606  sbthlem2  9020  findcard  9092  findcard2  9093  pssnn  9097  ssfi  9101  frfi  9189  unfilem3  9211  marypha1lem  9340  wemapso  9460  inf3lem3  9546  dfac9  10054  dfacacn  10059  kmlem11  10078  kmlem12  10079  fin23lem28  10257  isf32lem6  10275  isf32lem7  10276  isf32lem8  10277  domtriomlem  10359  axdc2lem  10365  axcclem  10374  zornn0g  10422  konigthlem  10486  grothprim  10752  hashbclem  14409  fi1uzind  14464  brfi1uzind  14465  brfi1indALT  14467  opfi1uzind  14468  ramub1lem1  16992  pltfval  18290  isirred  20394  cntzsdrg  20778  subdrgint  20779  lssset  20927  xrs1mnd  21419  xrs10  21420  xrs1cmn  21421  xrge0subm  21422  xrge0cmn  21423  cnmsgngrp  21558  psgninv  21561  psdmul  22158  neitr  23167  lecldbas  23206  imasdsf1olem  24360  xrge0gsumle  24821  xrge0tsms  24822  i1fd  25670  lhop1lem  26002  reefgim  26437  cxpcn2  26732  logbmpt  26774  newval  27849  newf  27852  addsval  27976  mulsval  28123  nnsex  28332  axlowdimlem15  29047  axlowdim  29052  elntg  29075  uhgrspan1lem1  29391  upgrres1lem1  29400  nbgrval  29427  nbfusgrlevtxm1  29468  cusgrfilem3  29548  vtxdginducedm1lem1  29630  vtxdginducedm1fi  29635  finsumvtxdg2ssteplem4  29639  padct  32814  rprmval  33611  dimkerim  33823  onvf1odlem2  35347  satfv1lem  35605  satfdm  35612  satffunlem1lem2  35646  satffunlem2lem2  35649  watvalN  40500  hvmapfval  42266  prjspval  43068  setindtr  43484  ssdifcl  44030  sssymdifcl  44031  clsk3nimkb  44499  iundjiunlem  46916  meaiuninclem  46937  meaiininclem  46943  lines  49236