Theorem difexi 5271

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906

This theorem is referenced by:  oev  8449  naddcllem  8612  sbthlem2  9026  findcard  9098  findcard2  9099  pssnn  9103  ssfi  9107  frfi  9195  unfilem3  9217  marypha1lem  9346  wemapso  9466  inf3lem3  9551  dfac9  10059  dfacacn  10064  kmlem11  10083  kmlem12  10084  fin23lem28  10262  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  domtriomlem  10364  axdc2lem  10370  axcclem  10379  zornn0g  10427  konigthlem  10491  grothprim  10757  hashbclem  14414  fi1uzind  14469  brfi1uzind  14470  brfi1indALT  14472  opfi1uzind  14473  ramub1lem1  16997  pltfval  18295  isirred  20399  cntzsdrg  20779  subdrgint  20780  lssset  20928  xrs1mnd  21420  xrs10  21421  xrs1cmn  21422  xrge0subm  21423  xrge0cmn  21424  cnmsgngrp  21559  psgninv  21562  psdmul  22132  neitr  23145  lecldbas  23184  imasdsf1olem  24338  xrge0gsumle  24799  xrge0tsms  24800  i1fd  25648  lhop1lem  25980  reefgim  26415  cxpcn2  26710  logbmpt  26752  newval  27827  newf  27830  addsval  27954  mulsval  28101  nnsex  28310  axlowdimlem15  29025  axlowdim  29030  elntg  29053  uhgrspan1lem1  29369  upgrres1lem1  29378  nbgrval  29405  nbfusgrlevtxm1  29446  cusgrfilem3  29526  vtxdginducedm1lem1  29608  vtxdginducedm1fi  29613  finsumvtxdg2ssteplem4  29617  padct  32791  rprmval  33576  dimkerim  33771  onvf1odlem2  35286  satfv1lem  35544  satfdm  35551  satffunlem1lem2  35585  satffunlem2lem2  35588  watvalN  40439  hvmapfval  42205  prjspval  43036  setindtr  43452  ssdifcl  43998  sssymdifcl  43999  clsk3nimkb  44467  iundjiunlem  46887  meaiuninclem  46908  meaiininclem  46914  lines  49207