Theorem difexi 5272

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437   ∖ cdif 3895

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-ss 3915

This theorem is referenced by:  oev  8438  naddcllem  8600  sbthlem2  9012  findcard  9084  findcard2  9085  pssnn  9089  ssfi  9093  frfi  9180  unfilem3  9202  marypha1lem  9328  wemapso  9448  inf3lem3  9531  dfac9  10039  dfacacn  10044  kmlem11  10063  kmlem12  10064  fin23lem28  10242  isf32lem6  10260  isf32lem7  10261  isf32lem8  10262  domtriomlem  10344  axdc2lem  10350  axcclem  10359  zornn0g  10407  konigthlem  10470  grothprim  10736  hashbclem  14366  fi1uzind  14421  brfi1uzind  14422  brfi1indALT  14424  opfi1uzind  14425  ramub1lem1  16945  pltfval  18243  isirred  20346  cntzsdrg  20726  subdrgint  20727  lssset  20875  xrs1mnd  21386  xrs10  21387  xrs1cmn  21388  xrge0subm  21389  xrge0cmn  21390  cnmsgngrp  21525  psgninv  21528  psdmul  22100  neitr  23115  lecldbas  23154  imasdsf1olem  24308  xrge0gsumle  24769  xrge0tsms  24770  i1fd  25629  lhop1lem  25965  reefgim  26407  cxpcn2  26703  logbmpt  26745  newval  27816  newf  27819  addsval  27925  mulsval  28068  nnsex  28267  axlowdimlem15  28955  axlowdim  28960  elntg  28983  uhgrspan1lem1  29299  upgrres1lem1  29308  nbgrval  29335  nbfusgrlevtxm1  29376  cusgrfilem3  29457  vtxdginducedm1lem1  29539  vtxdginducedm1fi  29544  finsumvtxdg2ssteplem4  29548  rprmval  33525  dimkerim  33712  onvf1odlem2  35220  satfv1lem  35478  satfdm  35485  satffunlem1lem2  35519  satffunlem2lem2  35522  watvalN  40165  hvmapfval  41931  prjspval  42761  setindtr  43181  ssdifcl  43728  sssymdifcl  43729  clsk3nimkb  44197  iundjiunlem  46619  meaiuninclem  46640  meaiininclem  46646  lines  48893