Theorem difexi 5299

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094

This theorem is used by:  oev  8560  naddcllem  8723  sbthlem2  9145  findcard  9217  findcard2  9218  pssnn  9222  ssfi  9226  frfi  9314  unfilem3  9337  marypha1lem  9462  wemapso  9582  inf3lem3  9668  dfac9  10254  dfacacn  10259  kmlem11  10278  kmlem12  10279  fin23lem28  10457  isf32lem6  10475  isf32lem7  10476  isf32lem8  10477  domtriomlem  10559  axdc2lem  10565  axcclem  10574  zornn0g  10622  konigthlem  10692  grothprim  10958  hashbclem  14638  fi1uzind  14693  brfi1uzind  14694  brfi1indALT  14696  opfi1uzind  14697  ramub1lem1  17248  pltfval  18553  isirred  20700  isdrng3lem1  21056  cntzsdrg  21110  subdrgint  21111  lssset  21259  xrs1mnd  21800  xrs10  21801  xrs1cmn  21802  xrge0subm  21803  xrge0cmn  21804  cnmsgngrp  21940  psgninv  21943  psdmul  22542  neitr  23553  lecldbas  23592  imasdsf1olem  24747  xrge0gsumle  25208  xrge0tsms  25209  i1fd  26057  lhop1lem  26388  reefgim  26834  cxpcn2  27131  logbmpt  27173  newval  28278  newf  28281  addsval  28405  mulsval  28552  nnsex  28761  tgplnfn  29310  plngval  29312  isplng  29313  axlowdimlem15  29591  axlowdim  29596  elntg  29619  uhgrspan1lem1  29938  upgrres1lem1  29947  nbgrval  29974  nbfusgrlevtxm1  30015  cusgrfilem3  30095  vtxdginducedm1lem1  30177  vtxdginducedm1fi  30182  finsumvtxdg2ssteplem4  30186  padct  33407  isedom  33953  rprmval  34152  dimkerim  34370  onvf1odlem2  36073  satfv1lem  36335  satfdm  36342  satffunlem1lem2  36376  satffunlem2lem2  36379  nmulprop  37154  watvalN  41316  hvmapfval  43082  prjspval  43897  setindtr  44297  ssdifcl  44833  sssymdifcl  44834  clsk3nimkb  45301  iundjiunlem  47742  meaiuninclem  47763  meaiininclem  47769  lines  50175