Theorem difexi 5288

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934

This theorem is referenced by:  oev  8481  naddcllem  8643  sbthlem2  9058  findcard  9133  findcard2  9134  pssnn  9138  ssfi  9143  frfi  9239  unfilem3  9263  marypha1lem  9391  wemapso  9511  inf3lem3  9590  dfac9  10097  dfacacn  10102  kmlem11  10121  kmlem12  10122  fin23lem28  10300  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  domtriomlem  10402  axdc2lem  10408  axcclem  10417  zornn0g  10465  konigthlem  10528  grothprim  10794  hashbclem  14424  fi1uzind  14479  brfi1uzind  14480  brfi1indALT  14482  opfi1uzind  14483  ramub1lem1  17004  pltfval  18297  isirred  20335  cntzsdrg  20718  subdrgint  20719  lssset  20846  xrs1mnd  21328  xrs10  21329  xrs1cmn  21330  xrge0subm  21331  xrge0cmn  21332  cnmsgngrp  21495  psgninv  21498  psdmul  22060  neitr  23074  lecldbas  23113  imasdsf1olem  24268  xrge0gsumle  24729  xrge0tsms  24730  i1fd  25589  lhop1lem  25925  reefgim  26367  cxpcn2  26663  logbmpt  26705  newval  27770  newf  27773  addsval  27876  mulsval  28019  nnsex  28218  axlowdimlem15  28890  axlowdim  28895  elntg  28918  uhgrspan1lem1  29234  upgrres1lem1  29243  nbgrval  29270  nbfusgrlevtxm1  29311  cusgrfilem3  29392  vtxdginducedm1lem1  29474  vtxdginducedm1fi  29479  finsumvtxdg2ssteplem4  29483  rprmval  33494  dimkerim  33630  onvf1odlem2  35098  satfv1lem  35356  satfdm  35363  satffunlem1lem2  35397  satffunlem2lem2  35400  watvalN  39994  hvmapfval  41760  prjspval  42598  setindtr  43020  ssdifcl  43567  sssymdifcl  43568  clsk3nimkb  44036  iundjiunlem  46464  meaiuninclem  46485  meaiininclem  46491  lines  48724