Theorem difexi 5335

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979

This theorem is referenced by:  oev  8550  naddcllem  8712  sbthlem2  9122  findcard  9201  findcard2  9202  pssnn  9206  ssfi  9211  phplem2OLD  9252  phpOLD  9256  frfi  9318  unfilem3  9342  marypha1lem  9470  wemapso  9588  inf3lem3  9667  dfac9  10174  dfacacn  10179  kmlem11  10198  kmlem12  10199  fin23lem28  10377  isf32lem6  10395  isf32lem7  10396  isf32lem8  10397  domtriomlem  10479  axdc2lem  10485  axcclem  10494  zornn0g  10542  konigthlem  10605  grothprim  10871  hashbclem  14487  fi1uzind  14542  brfi1uzind  14543  brfi1indALT  14545  opfi1uzind  14546  ramub1lem1  17059  pltfval  18388  isirred  20435  cntzsdrg  20819  subdrgint  20820  lssset  20948  xrs1mnd  21439  xrs10  21440  xrs1cmn  21441  xrge0subm  21442  xrge0cmn  21443  cnmsgngrp  21614  psgninv  21617  psdmul  22187  neitr  23203  lecldbas  23242  imasdsf1olem  24398  xrge0gsumle  24868  xrge0tsms  24869  i1fd  25729  lhop1lem  26066  reefgim  26508  cxpcn2  26803  logbmpt  26845  newval  27908  newf  27911  addsval  28009  mulsval  28149  nnsex  28337  axlowdimlem15  28985  axlowdim  28990  elntg  29013  uhgrspan1lem1  29331  upgrres1lem1  29340  nbgrval  29367  nbfusgrlevtxm1  29408  cusgrfilem3  29489  vtxdginducedm1lem1  29571  vtxdginducedm1fi  29576  finsumvtxdg2ssteplem4  29580  rprmval  33523  dimkerim  33654  satfv1lem  35346  satfdm  35353  satffunlem1lem2  35387  satffunlem2lem2  35390  watvalN  39975  hvmapfval  41741  prjspval  42589  setindtr  43012  ssdifcl  43560  sssymdifcl  43561  clsk3nimkb  44029  iundjiunlem  46414  meaiuninclem  46435  meaiininclem  46441  lines  48580