Theorem difexi 5283

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919

This theorem is referenced by:  oev  8477  naddcllem  8640  sbthlem2  9054  findcard  9126  findcard2  9127  pssnn  9131  ssfi  9135  frfi  9223  unfilem3  9245  marypha1lem  9373  wemapso  9493  inf3lem3  9579  dfac9  10087  dfacacn  10092  kmlem11  10111  kmlem12  10112  fin23lem28  10291  isf32lem6  10309  isf32lem7  10310  isf32lem8  10311  domtriomlem  10393  axdc2lem  10399  axcclem  10408  zornn0g  10456  konigthlem  10520  grothprim  10786  hashbclem  14459  fi1uzind  14514  brfi1uzind  14515  brfi1indALT  14517  opfi1uzind  14518  ramub1lem1  17053  pltfval  18352  isirred  20455  cntzsdrg  20839  subdrgint  20840  lssset  20988  xrs1mnd  21480  xrs10  21481  xrs1cmn  21482  xrge0subm  21483  xrge0cmn  21484  cnmsgngrp  21619  psgninv  21622  psdmul  22219  neitr  23228  lecldbas  23267  imasdsf1olem  24421  xrge0gsumle  24882  xrge0tsms  24883  i1fd  25731  lhop1lem  26063  reefgim  26501  cxpcn2  26799  logbmpt  26841  newval  27916  newf  27919  addsval  28043  mulsval  28190  nnsex  28399  axlowdimlem15  29114  axlowdim  29119  elntg  29142  uhgrspan1lem1  29458  upgrres1lem1  29467  nbgrval  29494  nbfusgrlevtxm1  29535  cusgrfilem3  29615  vtxdginducedm1lem1  29697  vtxdginducedm1fi  29702  finsumvtxdg2ssteplem4  29706  padct  32881  rprmval  33673  dimkerim  33885  onvf1odlem2  35408  satfv1lem  35673  satfdm  35680  satffunlem1lem2  35714  satffunlem2lem2  35717  nmulprop  36501  watvalN  40578  hvmapfval  42344  prjspval  43146  setindtr  43562  ssdifcl  44108  sssymdifcl  44109  clsk3nimkb  44577  iundjiunlem  46994  meaiuninclem  47015  meaiininclem  47021  lines  49314