Theorem difexg 5264

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-in 3897  df-ss 3907

This theorem is referenced by:  difexi  5265  difexd  5266  difex2  7710  elpwun  7719  2oconcl  8435  fnoe  8442  difsnen  8994  fodomr  9063  domss2  9071  domssex2  9072  domssex  9073  limenpsi  9087  dif1enlem  9091  sucdom2  9134  brwdom2  9485  infeq5i  9555  infdifsn  9576  dfac8clem  9952  ssfin4  10230  isf34lem1  10292  compssiso  10294  fin1a2lem7  10326  fin1a2lem13  10332  fpwwe2lem12  10563  hashgt23el  14384  pmtrfv  19425  isirred  20397  isdrng2  20722  drngmclOLD  20730  drngid2  20731  isdrngd  20744  isdrngdOLD  20746  subdrgint  20782  cnmsubglem  21412  islindf4  21820  smadiadetlem1a  22653  basdif0  22943  tgdif0  22982  clsval2  23040  cmpcld  23392  ptcmplem2  24043  iunmbl  25545  logbfval  26779  nbfusgrlevtxm2  29472  vtxdginducedm1  29637  frgrwopreglem1  30407  eigvecval  31992  elpwdifcl  32621  disjdifprg  32671  mptiffisupp  32792  resf1o  32829  xrge00  33100  xrge0tsmsd  33161  tocycf  33205  ist0cld  34024  locfinref  34032  ldsysgenld  34351  sigapildsys  34353  carsgclctun  34512  sitgclg  34533  ballotlemfrc  34718  ballotlem8  34728  bnj852  35110  bnj865  35112  subfacp1lem5  35419  iscvm  35494  cvmsval  35501  mdvval  35739  ttcwf2  36760  topdifinffinlem  37716  pibt2  37786  poimirlem15  38009  voliunnfl  38038  fdc  38119  isdrngo2  38332  lzenom  43226  diophin  43228  diophren  43265  deg1mhm  43652  stoweidlem57  46507  fourierdlem102  46658  fourierdlem114  46670  pwsal  46765  gsumge0cl  46821  caragendifcl  46964  carageniuncllem1  46971  isomenndlem  46980  hoidmv1lelem2  47042  lincdifsn  48922  lindslinindsimp1  48955  lindslinindimp2lem2  48957  lindslinindimp2lem4  48959  lindslinindsimp2lem5  48960  lindslinindsimp2  48961  lincresunit1  48975  lincresunit2  48976  lincresunit3lem2  48978  lincresunit3  48979