Theorem difexi 5258

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  oev  8439  naddcllem  8602  sbthlem2  9016  findcard  9088  findcard2  9089  pssnn  9093  ssfi  9097  frfi  9185  unfilem3  9207  marypha1lem  9336  wemapso  9456  inf3lem3  9542  dfac9  10050  dfacacn  10055  kmlem11  10074  kmlem12  10075  fin23lem28  10253  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  domtriomlem  10355  axdc2lem  10361  axcclem  10370  zornn0g  10418  konigthlem  10482  grothprim  10748  hashbclem  14405  fi1uzind  14460  brfi1uzind  14461  brfi1indALT  14463  opfi1uzind  14464  ramub1lem1  16988  pltfval  18286  isirred  20390  cntzsdrg  20774  subdrgint  20775  lssset  20923  xrs1mnd  21415  xrs10  21416  xrs1cmn  21417  xrge0subm  21418  xrge0cmn  21419  cnmsgngrp  21554  psgninv  21557  psdmul  22154  neitr  23163  lecldbas  23202  imasdsf1olem  24356  xrge0gsumle  24817  xrge0tsms  24818  i1fd  25666  lhop1lem  25998  reefgim  26433  cxpcn2  26728  logbmpt  26770  newval  27845  newf  27848  addsval  27972  mulsval  28119  nnsex  28328  axlowdimlem15  29043  axlowdim  29048  elntg  29071  uhgrspan1lem1  29387  upgrres1lem1  29396  nbgrval  29423  nbfusgrlevtxm1  29464  cusgrfilem3  29544  vtxdginducedm1lem1  29626  vtxdginducedm1fi  29631  finsumvtxdg2ssteplem4  29635  padct  32810  rprmval  33599  dimkerim  33811  onvf1odlem2  35332  satfv1lem  35590  satfdm  35597  satffunlem1lem2  35631  satffunlem2lem2  35634  watvalN  40485  hvmapfval  42251  prjspval  43053  setindtr  43469  ssdifcl  44015  sssymdifcl  44016  clsk3nimkb  44484  iundjiunlem  46902  meaiuninclem  46923  meaiininclem  46929  lines  49222