Theorem difexi 5292

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ∖ cdif 3896

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916

This theorem is used by:  oev  8515  naddcllem  8678  sbthlem2  9100  findcard  9172  findcard2  9173  pssnn  9177  ssfi  9181  frfi  9269  unfilem3  9292  marypha1lem  9418  wemapso  9538  inf3lem3  9624  dfac9  10208  dfacacn  10213  kmlem11  10232  kmlem12  10233  fin23lem28  10411  isf32lem6  10429  isf32lem7  10430  isf32lem8  10431  domtriomlem  10513  axdc2lem  10519  axcclem  10528  zornn0g  10576  konigthlem  10646  grothprim  10912  hashbclem  14590  fi1uzind  14645  brfi1uzind  14646  brfi1indALT  14648  opfi1uzind  14649  ramub1lem1  17197  pltfval  18496  isirred  20642  isdrng3lem1  20998  cntzsdrg  21052  subdrgint  21053  lssset  21201  xrs1mnd  21739  xrs10  21740  xrs1cmn  21741  xrge0subm  21742  xrge0cmn  21743  cnmsgngrp  21878  psgninv  21881  psdmul  22480  neitr  23491  lecldbas  23530  imasdsf1olem  24685  xrge0gsumle  25146  xrge0tsms  25147  i1fd  25995  lhop1lem  26326  reefgim  26770  cxpcn2  27067  logbmpt  27109  newval  28214  newf  28217  addsval  28341  mulsval  28488  nnsex  28697  tgplnfn  29246  plngval  29248  isplng  29249  axlowdimlem15  29527  axlowdim  29532  elntg  29555  uhgrspan1lem1  29874  upgrres1lem1  29883  nbgrval  29910  nbfusgrlevtxm1  29951  cusgrfilem3  30031  vtxdginducedm1lem1  30113  vtxdginducedm1fi  30118  finsumvtxdg2ssteplem4  30122  padct  33303  rprmval  34041  dimkerim  34252  onvf1odlem2  35866  satfv1lem  36106  satfdm  36113  satffunlem1lem2  36147  satffunlem2lem2  36150  nmulprop  36919  watvalN  41030  hvmapfval  42796  prjspval  43611  setindtr  44010  ssdifcl  44556  sssymdifcl  44557  clsk3nimkb  45025  iundjiunlem  47438  meaiuninclem  47459  meaiininclem  47465  lines  49812