Theorem difexi 5285

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931

This theorem is referenced by:  oev  8478  naddcllem  8640  sbthlem2  9052  findcard  9127  findcard2  9128  pssnn  9132  ssfi  9137  frfi  9232  unfilem3  9256  marypha1lem  9384  wemapso  9504  inf3lem3  9583  dfac9  10090  dfacacn  10095  kmlem11  10114  kmlem12  10115  fin23lem28  10293  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  domtriomlem  10395  axdc2lem  10401  axcclem  10410  zornn0g  10458  konigthlem  10521  grothprim  10787  hashbclem  14417  fi1uzind  14472  brfi1uzind  14473  brfi1indALT  14475  opfi1uzind  14476  ramub1lem1  16997  pltfval  18290  isirred  20328  cntzsdrg  20711  subdrgint  20712  lssset  20839  xrs1mnd  21321  xrs10  21322  xrs1cmn  21323  xrge0subm  21324  xrge0cmn  21325  cnmsgngrp  21488  psgninv  21491  psdmul  22053  neitr  23067  lecldbas  23106  imasdsf1olem  24261  xrge0gsumle  24722  xrge0tsms  24723  i1fd  25582  lhop1lem  25918  reefgim  26360  cxpcn2  26656  logbmpt  26698  newval  27763  newf  27766  addsval  27869  mulsval  28012  nnsex  28211  axlowdimlem15  28883  axlowdim  28888  elntg  28911  uhgrspan1lem1  29227  upgrres1lem1  29236  nbgrval  29263  nbfusgrlevtxm1  29304  cusgrfilem3  29385  vtxdginducedm1lem1  29467  vtxdginducedm1fi  29472  finsumvtxdg2ssteplem4  29476  rprmval  33487  dimkerim  33623  onvf1odlem2  35091  satfv1lem  35349  satfdm  35356  satffunlem1lem2  35390  satffunlem2lem2  35393  watvalN  39987  hvmapfval  41753  prjspval  42591  setindtr  43013  ssdifcl  43560  sssymdifcl  43561  clsk3nimkb  44029  iundjiunlem  46457  meaiuninclem  46478  meaiininclem  46484  lines  48720