Theorem difexi 5298

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-in 3920  df-ss 3930

This theorem is referenced by:  oev  8495  naddcllem  8658  sbthlem2  9072  findcard  9144  findcard2  9145  pssnn  9149  ssfi  9153  frfi  9241  unfilem3  9263  marypha1lem  9389  wemapso  9509  inf3lem3  9595  dfac9  10116  dfacacn  10121  kmlem11  10140  kmlem12  10141  fin23lem28  10320  isf32lem6  10338  isf32lem7  10339  isf32lem8  10340  domtriomlem  10422  axdc2lem  10428  axcclem  10437  zornn0g  10485  konigthlem  10549  grothprim  10815  hashbclem  14485  fi1uzind  14540  brfi1uzind  14541  brfi1indALT  14543  opfi1uzind  14544  ramub1lem1  17082  pltfval  18381  isirred  20497  cntzsdrg  20879  subdrgint  20880  lssset  21028  xrs1mnd  21555  xrs10  21556  xrs1cmn  21557  xrge0subm  21558  xrge0cmn  21559  cnmsgngrp  21694  psgninv  21697  psdmul  22294  neitr  23302  lecldbas  23341  imasdsf1olem  24495  xrge0gsumle  24956  xrge0tsms  24957  i1fd  25805  lhop1lem  26137  reefgim  26575  cxpcn2  26873  logbmpt  26915  newval  27990  newf  27993  addsval  28117  mulsval  28264  nnsex  28473  tgplnfn  29011  plngval  29013  isplng  29014  axlowdimlem15  29243  axlowdim  29248  elntg  29271  uhgrspan1lem1  29587  upgrres1lem1  29596  nbgrval  29623  nbfusgrlevtxm1  29664  cusgrfilem3  29744  vtxdginducedm1lem1  29826  vtxdginducedm1fi  29831  finsumvtxdg2ssteplem4  29835  padct  33000  rprmval  33747  dimkerim  33958  onvf1odlem2  35483  satfv1lem  35749  satfdm  35756  satffunlem1lem2  35790  satffunlem2lem2  35793  nmulprop  36577  watvalN  40652  hvmapfval  42418  prjspval  43222  setindtr  43638  ssdifcl  44184  sssymdifcl  44185  clsk3nimkb  44653  iundjiunlem  47060  meaiuninclem  47081  meaiininclem  47087  lines  49391