Theorem difexg 5279

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 4095	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5273	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911

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 5246

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 3403  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928

This theorem is referenced by:  difexi  5280  difexd  5281  difex2  7716  elpwun  7725  2oconcl  8444  fnoe  8451  difsnen  9000  fodomr  9069  domss2  9077  domssex2  9078  domssex  9079  limenpsi  9093  dif1enlem  9097  sucdom2  9144  brwdom2  9502  infeq5i  9565  infdifsn  9586  dfac8clem  9961  ssfin4  10239  isf34lem1  10301  compssiso  10303  fin1a2lem7  10335  fin1a2lem13  10341  fpwwe2lem12  10571  hashgt23el  14365  pmtrfv  19358  isirred  20304  isdrng2  20628  drngmclOLD  20636  drngid2  20637  isdrngd  20650  isdrngdOLD  20652  subdrgint  20688  cnmsubglem  21323  islindf4  21723  smadiadetlem1a  22526  basdif0  22816  tgdif0  22855  clsval2  22913  cmpcld  23265  ptcmplem2  23916  iunmbl  25430  logbfval  26676  nbfusgrlevtxm2  29281  vtxdginducedm1  29447  frgrwopreglem1  30214  eigvecval  31798  elpwdifcl  32428  disjdifprg  32477  mptiffisupp  32589  padct  32616  resf1o  32626  xrge00  32926  xrge0tsmsd  32975  tocycf  33047  ist0cld  33796  locfinref  33804  ldsysgenld  34123  sigapildsys  34125  carsgclctun  34285  sitgclg  34306  ballotlemfrc  34491  ballotlem8  34501  bnj852  34884  bnj865  34886  subfacp1lem5  35144  iscvm  35219  cvmsval  35226  mdvval  35464  topdifinffinlem  37308  pibt2  37378  poimirlem15  37602  voliunnfl  37631  fdc  37712  isdrngo2  37925  lzenom  42731  diophin  42733  diophren  42774  deg1mhm  43162  stoweidlem57  46028  fourierdlem102  46179  fourierdlem114  46191  pwsal  46286  gsumge0cl  46342  caragendifcl  46485  carageniuncllem1  46492  isomenndlem  46501  hoidmv1lelem2  46563  lincdifsn  48386  lindslinindsimp1  48419  lindslinindimp2lem2  48421  lindslinindimp2lem4  48423  lindslinindsimp2lem5  48424  lindslinindsimp2  48425  lincresunit1  48439  lincresunit2  48440  lincresunit3lem2  48442  lincresunit3  48443