Theorem difexi 5247

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  oev  8306  sbthlem2  8824  phplem2  8893  php  8897  findcard  8908  findcard2  8909  pssnn  8913  ssfi  8918  pssnnOLD  8969  findcard2OLD  8986  frfi  8989  unfilem3  9010  marypha1lem  9122  wemapso  9240  inf3lem3  9318  dfac9  9823  dfacacn  9828  kmlem11  9847  kmlem12  9848  fin23lem28  10027  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  domtriomlem  10129  axdc2lem  10135  axcclem  10144  zornn0g  10192  konigthlem  10255  grothprim  10521  hashbclem  14092  fi1uzind  14139  brfi1uzind  14140  brfi1indALT  14142  opfi1uzind  14143  ramub1lem1  16655  pltfval  17964  isirred  19856  cntzsdrg  19985  subdrgint  19986  lssset  20110  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  xrge0subm  20551  xrge0cmn  20552  cnmsgngrp  20696  psgninv  20699  neitr  22239  lecldbas  22278  imasdsf1olem  23434  xrge0gsumle  23902  xrge0tsms  23903  i1fd  24750  lhop1lem  25082  reefgim  25514  cxpcn2  25804  logbmpt  25843  axlowdimlem15  27227  axlowdim  27232  elntg  27255  uhgrspan1lem1  27570  upgrres1lem1  27579  nbgrval  27606  nbfusgrlevtxm1  27647  cusgrfilem3  27727  vtxdginducedm1lem1  27809  vtxdginducedm1fi  27814  finsumvtxdg2ssteplem4  27818  rprmval  31566  dimkerim  31610  satfv1lem  33224  satfdm  33231  satffunlem1lem2  33265  satffunlem2lem2  33268  naddcllem  33758  newval  33966  newf  33969  addsval  34053  watvalN  37934  hvmapfval  39700  prjspval  40363  setindtr  40762  ssdifcl  41067  sssymdifcl  41068  clsk3nimkb  41539  iundjiunlem  43887  meaiuninclem  43908  meaiininclem  43914  lines  45965