Theorem difexi 5275

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∖ cdif 3898

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 2708  ax-sep 5241

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908  df-ss 3918

This theorem is referenced by:  oev  8441  naddcllem  8604  sbthlem2  9016  findcard  9088  findcard2  9089  pssnn  9093  ssfi  9097  frfi  9185  unfilem3  9207  marypha1lem  9336  wemapso  9456  inf3lem3  9539  dfac9  10047  dfacacn  10052  kmlem11  10071  kmlem12  10072  fin23lem28  10250  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  domtriomlem  10352  axdc2lem  10358  axcclem  10367  zornn0g  10415  konigthlem  10479  grothprim  10745  hashbclem  14375  fi1uzind  14430  brfi1uzind  14431  brfi1indALT  14433  opfi1uzind  14434  ramub1lem1  16954  pltfval  18252  isirred  20355  cntzsdrg  20735  subdrgint  20736  lssset  20884  xrs1mnd  21395  xrs10  21396  xrs1cmn  21397  xrge0subm  21398  xrge0cmn  21399  cnmsgngrp  21534  psgninv  21537  psdmul  22109  neitr  23124  lecldbas  23163  imasdsf1olem  24317  xrge0gsumle  24778  xrge0tsms  24779  i1fd  25638  lhop1lem  25974  reefgim  26416  cxpcn2  26712  logbmpt  26754  newval  27831  newf  27834  addsval  27958  mulsval  28105  nnsex  28314  axlowdimlem15  29029  axlowdim  29034  elntg  29057  uhgrspan1lem1  29373  upgrres1lem1  29382  nbgrval  29409  nbfusgrlevtxm1  29450  cusgrfilem3  29531  vtxdginducedm1lem1  29613  vtxdginducedm1fi  29618  finsumvtxdg2ssteplem4  29622  rprmval  33597  dimkerim  33784  onvf1odlem2  35298  satfv1lem  35556  satfdm  35563  satffunlem1lem2  35597  satffunlem2lem2  35600  watvalN  40253  hvmapfval  42019  prjspval  42846  setindtr  43266  ssdifcl  43812  sssymdifcl  43813  clsk3nimkb  44281  iundjiunlem  46703  meaiuninclem  46724  meaiininclem  46730  lines  48977