Theorem difexi 5232

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ∖ cdif 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  oev  8139  sbthlem2  8628  phplem2  8697  php  8701  pssnn  8736  findcard  8757  findcard2  8758  frfi  8763  unfilem3  8784  marypha1lem  8897  inf3lem3  9093  dfac9  9562  dfacacn  9567  kmlem11  9586  kmlem12  9587  fin23lem28  9762  isf32lem6  9780  isf32lem7  9781  isf32lem8  9782  domtriomlem  9864  axdc2lem  9870  axcclem  9879  zornn0g  9927  konigthlem  9990  grothprim  10256  hashbclem  13811  fi1uzind  13856  brfi1uzind  13857  opfi1uzind  13860  ramub1lem1  16362  pltfval  17569  isirred  19449  cntzsdrg  19581  subdrgint  19582  lssset  19705  xrs1mnd  20583  xrs10  20584  xrs1cmn  20585  xrge0subm  20586  xrge0cmn  20587  cnmsgngrp  20723  psgninv  20726  neitr  21788  lecldbas  21827  imasdsf1olem  22983  xrge0gsumle  23441  xrge0tsms  23442  i1fd  24282  lhop1lem  24610  reefgim  25038  cxpcn2  25327  logbmpt  25366  axlowdimlem15  26742  axlowdim  26747  elntg  26770  uhgrspan1lem1  27082  upgrres1lem1  27091  nbgrval  27118  nbfusgrlevtxm1  27159  cusgrfilem3  27239  vtxdginducedm1lem1  27321  vtxdginducedm1fi  27326  finsumvtxdg2ssteplem4  27330  dimkerim  31023  satfv1lem  32609  satfdm  32616  satffunlem1lem2  32650  satffunlem2lem2  32653  watvalN  37144  hvmapfval  38910  prjspval  39273  setindtr  39641  ssdifcl  39950  sssymdifcl  39951  clsk3nimkb  40410  meaiuninclem  42782  meaiininclem  42788  lines  44738