Theorem difexi 5327

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

Syntax hints:   ∈ wcel 2099  Vcvv 3464   ∖ cdif 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3421  df-v 3466  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  oev  8535  naddcllem  8697  sbthlem2  9113  findcard  9192  findcard2  9193  pssnn  9197  ssfi  9203  phplem2OLD  9244  phpOLD  9248  pssnnOLD  9291  findcard2OLD  9310  frfi  9314  unfilem3  9338  marypha1lem  9468  wemapso  9586  inf3lem3  9665  dfac9  10171  dfacacn  10176  kmlem11  10195  kmlem12  10196  fin23lem28  10373  isf32lem6  10391  isf32lem7  10392  isf32lem8  10393  domtriomlem  10475  axdc2lem  10481  axcclem  10490  zornn0g  10538  konigthlem  10601  grothprim  10867  hashbclem  14463  fi1uzind  14510  brfi1uzind  14511  brfi1indALT  14513  opfi1uzind  14514  ramub1lem1  17022  pltfval  18350  isirred  20396  cntzsdrg  20776  subdrgint  20777  lssset  20905  xrs1mnd  21396  xrs10  21397  xrs1cmn  21398  xrge0subm  21399  xrge0cmn  21400  cnmsgngrp  21570  psgninv  21573  psdmul  22155  neitr  23171  lecldbas  23210  imasdsf1olem  24366  xrge0gsumle  24836  xrge0tsms  24837  i1fd  25697  lhop1lem  26033  reefgim  26476  cxpcn2  26770  logbmpt  26812  newval  27875  newf  27878  addsval  27972  mulsval  28106  nnsex  28287  axlowdimlem15  28886  axlowdim  28891  elntg  28914  uhgrspan1lem1  29232  upgrres1lem1  29241  nbgrval  29268  nbfusgrlevtxm1  29309  cusgrfilem3  29390  vtxdginducedm1lem1  29472  vtxdginducedm1fi  29477  finsumvtxdg2ssteplem4  29481  rprmval  33396  dimkerim  33527  satfv1lem  35202  satfdm  35209  satffunlem1lem2  35243  satffunlem2lem2  35246  watvalN  39704  hvmapfval  41470  prjspval  42292  setindtr  42718  ssdifcl  43274  sssymdifcl  43275  clsk3nimkb  43743  iundjiunlem  46115  meaiuninclem  46136  meaiininclem  46142  lines  48154