Theorem difexi 5303

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-in 3913  df-ss 3923

This theorem is used by:  oev  8501  naddcllem  8664  sbthlem2  9079  findcard  9151  findcard2  9152  pssnn  9156  ssfi  9160  frfi  9248  unfilem3  9270  marypha1lem  9396  wemapso  9516  inf3lem3  9602  dfac9  10132  dfacacn  10137  kmlem11  10156  kmlem12  10157  fin23lem28  10335  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  domtriomlem  10437  axdc2lem  10443  axcclem  10452  zornn0g  10500  konigthlem  10564  grothprim  10830  hashbclem  14503  fi1uzind  14558  brfi1uzind  14559  brfi1indALT  14561  opfi1uzind  14562  ramub1lem1  17104  pltfval  18403  isirred  20527  isdrng3lem1  20881  cntzsdrg  20935  subdrgint  20936  lssset  21084  xrs1mnd  21620  xrs10  21621  xrs1cmn  21622  xrge0subm  21623  xrge0cmn  21624  cnmsgngrp  21759  psgninv  21762  psdmul  22359  neitr  23367  lecldbas  23406  imasdsf1olem  24561  xrge0gsumle  25022  xrge0tsms  25023  i1fd  25871  lhop1lem  26203  reefgim  26644  cxpcn2  26942  logbmpt  26984  newval  28059  newf  28062  addsval  28186  mulsval  28333  nnsex  28542  tgplnfn  29088  plngval  29090  isplng  29091  axlowdimlem15  29337  axlowdim  29342  elntg  29365  uhgrspan1lem1  29684  upgrres1lem1  29693  nbgrval  29720  nbfusgrlevtxm1  29761  cusgrfilem3  29841  vtxdginducedm1lem1  29923  vtxdginducedm1fi  29928  finsumvtxdg2ssteplem4  29932  padct  33109  rprmval  33846  dimkerim  34057  onvf1odlem2  35621  satfv1lem  35867  satfdm  35874  satffunlem1lem2  35908  satffunlem2lem2  35911  nmulprop  36695  watvalN  40800  hvmapfval  42566  prjspval  43368  setindtr  43784  ssdifcl  44330  sssymdifcl  44331  clsk3nimkb  44799  iundjiunlem  47206  meaiuninclem  47227  meaiininclem  47233  lines  49544