Theorem difexi 5295

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-in 3906  df-ss 3916

This theorem is used by:  oev  8501  naddcllem  8664  sbthlem2  9086  findcard  9158  findcard2  9159  pssnn  9163  ssfi  9167  frfi  9255  unfilem3  9277  marypha1lem  9403  wemapso  9523  inf3lem3  9609  dfac9  10139  dfacacn  10144  kmlem11  10163  kmlem12  10164  fin23lem28  10342  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  domtriomlem  10444  axdc2lem  10450  axcclem  10459  zornn0g  10507  konigthlem  10577  grothprim  10843  hashbclem  14517  fi1uzind  14572  brfi1uzind  14573  brfi1indALT  14575  opfi1uzind  14576  ramub1lem1  17118  pltfval  18417  isirred  20560  isdrng3lem1  20914  cntzsdrg  20968  subdrgint  20969  lssset  21117  xrs1mnd  21653  xrs10  21654  xrs1cmn  21655  xrge0subm  21656  xrge0cmn  21657  cnmsgngrp  21792  psgninv  21795  psdmul  22394  neitr  23405  lecldbas  23444  imasdsf1olem  24599  xrge0gsumle  25060  xrge0tsms  25061  i1fd  25909  lhop1lem  26240  reefgim  26686  cxpcn2  26983  logbmpt  27025  newval  28100  newf  28103  addsval  28227  mulsval  28374  nnsex  28583  tgplnfn  29132  plngval  29134  isplng  29135  axlowdimlem15  29413  axlowdim  29418  elntg  29441  uhgrspan1lem1  29760  upgrres1lem1  29769  nbgrval  29796  nbfusgrlevtxm1  29837  cusgrfilem3  29917  vtxdginducedm1lem1  29999  vtxdginducedm1fi  30004  finsumvtxdg2ssteplem4  30008  padct  33189  rprmval  33926  dimkerim  34137  onvf1odlem2  35701  satfv1lem  35941  satfdm  35948  satffunlem1lem2  35982  satffunlem2lem2  35985  nmulprop  36770  watvalN  40866  hvmapfval  42632  prjspval  43449  setindtr  43865  ssdifcl  44411  sssymdifcl  44412  clsk3nimkb  44880  iundjiunlem  47287  meaiuninclem  47308  meaiininclem  47314  lines  49661