Theorem difexi 5291

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090

This theorem is used by:  oev  8527  naddcllem  8690  sbthlem2  9112  findcard  9184  findcard2  9185  pssnn  9189  ssfi  9193  frfi  9281  unfilem3  9304  marypha1lem  9430  wemapso  9550  inf3lem3  9636  dfac9  10220  dfacacn  10225  kmlem11  10244  kmlem12  10245  fin23lem28  10423  isf32lem6  10441  isf32lem7  10442  isf32lem8  10443  domtriomlem  10525  axdc2lem  10531  axcclem  10540  zornn0g  10588  konigthlem  10658  grothprim  10924  hashbclem  14602  fi1uzind  14657  brfi1uzind  14658  brfi1indALT  14660  opfi1uzind  14661  ramub1lem1  17211  pltfval  18510  isirred  20656  isdrng3lem1  21012  cntzsdrg  21066  subdrgint  21067  lssset  21215  xrs1mnd  21753  xrs10  21754  xrs1cmn  21755  xrge0subm  21756  xrge0cmn  21757  cnmsgngrp  21892  psgninv  21895  psdmul  22494  neitr  23505  lecldbas  23544  imasdsf1olem  24699  xrge0gsumle  25160  xrge0tsms  25161  i1fd  26009  lhop1lem  26340  reefgim  26784  cxpcn2  27081  logbmpt  27123  newval  28228  newf  28231  addsval  28355  mulsval  28502  nnsex  28711  tgplnfn  29260  plngval  29262  isplng  29263  axlowdimlem15  29541  axlowdim  29546  elntg  29569  uhgrspan1lem1  29888  upgrres1lem1  29897  nbgrval  29924  nbfusgrlevtxm1  29965  cusgrfilem3  30045  vtxdginducedm1lem1  30127  vtxdginducedm1fi  30132  finsumvtxdg2ssteplem4  30136  padct  33359  rprmval  34096  dimkerim  34307  onvf1odlem2  35953  satfv1lem  36215  satfdm  36222  satffunlem1lem2  36256  satffunlem2lem2  36259  nmulprop  37033  watvalN  41157  hvmapfval  42923  prjspval  43738  setindtr  44138  ssdifcl  44679  sssymdifcl  44680  clsk3nimkb  45147  iundjiunlem  47576  meaiuninclem  47597  meaiininclem  47603  lines  49951