Theorem difexg 5271

Description: Existence of a difference. (Contributed by NM, 26-May-1998.)

Assertion

Ref	Expression
difexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Proof of Theorem difexg

Step	Hyp	Ref	Expression
1		difss 4089	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5265	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922

This theorem is referenced by:  difexi  5272  difexd  5273  difex2  7700  elpwun  7709  2oconcl  8428  fnoe  8435  difsnen  8983  fodomr  9052  domss2  9060  domssex2  9061  domssex  9062  limenpsi  9076  dif1enlem  9080  sucdom2  9127  brwdom2  9484  infeq5i  9551  infdifsn  9572  dfac8clem  9945  ssfin4  10223  isf34lem1  10285  compssiso  10287  fin1a2lem7  10319  fin1a2lem13  10325  fpwwe2lem12  10555  hashgt23el  14349  pmtrfv  19349  isirred  20322  isdrng2  20646  drngmclOLD  20654  drngid2  20655  isdrngd  20668  isdrngdOLD  20670  subdrgint  20706  cnmsubglem  21355  islindf4  21763  smadiadetlem1a  22566  basdif0  22856  tgdif0  22895  clsval2  22953  cmpcld  23305  ptcmplem2  23956  iunmbl  25470  logbfval  26716  nbfusgrlevtxm2  29341  vtxdginducedm1  29507  frgrwopreglem1  30274  eigvecval  31858  elpwdifcl  32488  disjdifprg  32537  mptiffisupp  32649  padct  32676  resf1o  32686  xrge00  32981  xrge0tsmsd  33028  tocycf  33072  ist0cld  33802  locfinref  33810  ldsysgenld  34129  sigapildsys  34131  carsgclctun  34291  sitgclg  34312  ballotlemfrc  34497  ballotlem8  34507  bnj852  34890  bnj865  34892  subfacp1lem5  35159  iscvm  35234  cvmsval  35241  mdvval  35479  topdifinffinlem  37323  pibt2  37393  poimirlem15  37617  voliunnfl  37646  fdc  37727  isdrngo2  37940  lzenom  42746  diophin  42748  diophren  42789  deg1mhm  43176  stoweidlem57  46042  fourierdlem102  46193  fourierdlem114  46205  pwsal  46300  gsumge0cl  46356  caragendifcl  46499  carageniuncllem1  46506  isomenndlem  46515  hoidmv1lelem2  46577  lincdifsn  48413  lindslinindsimp1  48446  lindslinindimp2lem2  48448  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lincresunit1  48466  lincresunit2  48467  lincresunit3lem2  48469  lincresunit3  48470