Theorem difexi 5223

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

Syntax hints:   ∈ wcel 2108  Vcvv 3493   ∖ cdif 3931

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 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-in 3941  df-ss 3950

This theorem is referenced by:  oev  8131  sbthlem2  8620  phplem2  8689  php  8693  pssnn  8728  findcard  8749  findcard2  8750  frfi  8755  unfilem3  8776  marypha1lem  8889  inf3lem3  9085  dfac9  9554  dfacacn  9559  kmlem11  9578  kmlem12  9579  fin23lem28  9754  isf32lem6  9772  isf32lem7  9773  isf32lem8  9774  domtriomlem  9856  axdc2lem  9862  axcclem  9871  zornn0g  9919  konigthlem  9982  grothprim  10248  hashbclem  13802  fi1uzind  13847  brfi1uzind  13848  opfi1uzind  13851  ramub1lem1  16354  pltfval  17561  isirred  19441  cntzsdrg  19573  subdrgint  19574  lssset  19697  xrs1mnd  20575  xrs10  20576  xrs1cmn  20577  xrge0subm  20578  xrge0cmn  20579  cnmsgngrp  20715  psgninv  20718  neitr  21780  lecldbas  21819  imasdsf1olem  22975  xrge0gsumle  23433  xrge0tsms  23434  i1fd  24274  lhop1lem  24602  reefgim  25030  cxpcn2  25319  logbmpt  25358  axlowdimlem15  26734  axlowdim  26739  elntg  26762  uhgrspan1lem1  27074  upgrres1lem1  27083  nbgrval  27110  nbfusgrlevtxm1  27151  cusgrfilem3  27231  vtxdginducedm1lem1  27313  vtxdginducedm1fi  27318  finsumvtxdg2ssteplem4  27322  dimkerim  31016  satfv1lem  32602  satfdm  32609  satffunlem1lem2  32643  satffunlem2lem2  32646  watvalN  37121  hvmapfval  38887  prjspval  39243  0prjspn  39260  setindtr  39611  ssdifcl  39920  sssymdifcl  39921  clsk3nimkb  40380  meaiuninclem  42752  meaiininclem  42758  lines  44708