Theorem difexi 5196

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898

This theorem is referenced by:  oev  8122  sbthlem2  8612  phplem2  8681  php  8685  pssnn  8720  findcard  8741  findcard2  8742  frfi  8747  unfilem3  8768  marypha1lem  8881  inf3lem3  9077  dfac9  9547  dfacacn  9552  kmlem11  9571  kmlem12  9572  fin23lem28  9751  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  domtriomlem  9853  axdc2lem  9859  axcclem  9868  zornn0g  9916  konigthlem  9979  grothprim  10245  hashbclem  13806  fi1uzind  13851  brfi1uzind  13852  brfi1indALT  13854  opfi1uzind  13855  ramub1lem1  16352  pltfval  17561  isirred  19445  cntzsdrg  19574  subdrgint  19575  lssset  19698  xrs1mnd  20129  xrs10  20130  xrs1cmn  20131  xrge0subm  20132  xrge0cmn  20133  cnmsgngrp  20268  psgninv  20271  neitr  21785  lecldbas  21824  imasdsf1olem  22980  xrge0gsumle  23438  xrge0tsms  23439  i1fd  24285  lhop1lem  24616  reefgim  25045  cxpcn2  25335  logbmpt  25374  axlowdimlem15  26750  axlowdim  26755  elntg  26778  uhgrspan1lem1  27090  upgrres1lem1  27099  nbgrval  27126  nbfusgrlevtxm1  27167  cusgrfilem3  27247  vtxdginducedm1lem1  27329  vtxdginducedm1fi  27334  finsumvtxdg2ssteplem4  27338  rprmval  31072  dimkerim  31111  satfv1lem  32722  satfdm  32729  satffunlem1lem2  32763  satffunlem2lem2  32766  watvalN  37289  hvmapfval  39055  prjspval  39597  setindtr  39965  ssdifcl  40270  sssymdifcl  40271  clsk3nimkb  40743  iundjiunlem  43098  meaiuninclem  43119  meaiininclem  43125  lines  45145