Theorem difexg 5270

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906

This theorem is referenced by:  difexi  5271  difexd  5272  difex2  7714  elpwun  7723  2oconcl  8438  fnoe  8445  difsnen  8997  fodomr  9066  domss2  9074  domssex2  9075  domssex  9076  limenpsi  9090  dif1enlem  9094  sucdom2  9137  brwdom2  9488  infeq5i  9557  infdifsn  9578  dfac8clem  9954  ssfin4  10232  isf34lem1  10294  compssiso  10296  fin1a2lem7  10328  fin1a2lem13  10334  fpwwe2lem12  10565  hashgt23el  14386  pmtrfv  19427  isirred  20399  isdrng2  20720  drngmclOLD  20728  drngid2  20729  isdrngd  20742  isdrngdOLD  20744  subdrgint  20780  cnmsubglem  21410  islindf4  21818  smadiadetlem1a  22628  basdif0  22918  tgdif0  22957  clsval2  23015  cmpcld  23367  ptcmplem2  24018  iunmbl  25520  logbfval  26754  nbfusgrlevtxm2  29447  vtxdginducedm1  29612  frgrwopreglem1  30382  eigvecval  31967  elpwdifcl  32596  disjdifprg  32645  mptiffisupp  32766  resf1o  32803  xrge00  33074  xrge0tsmsd  33134  tocycf  33178  ist0cld  33977  locfinref  33985  ldsysgenld  34304  sigapildsys  34306  carsgclctun  34465  sitgclg  34486  ballotlemfrc  34671  ballotlem8  34681  bnj852  35063  bnj865  35065  subfacp1lem5  35366  iscvm  35441  cvmsval  35448  mdvval  35686  ttcwf2  36707  topdifinffinlem  37663  pibt2  37733  poimirlem15  37956  voliunnfl  37985  fdc  38066  isdrngo2  38279  lzenom  43202  diophin  43204  diophren  43241  deg1mhm  43628  stoweidlem57  46485  fourierdlem102  46636  fourierdlem114  46648  pwsal  46743  gsumge0cl  46799  caragendifcl  46942  carageniuncllem1  46949  isomenndlem  46958  hoidmv1lelem2  47020  lincdifsn  48900  lindslinindsimp1  48933  lindslinindimp2lem2  48935  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  lincresunit1  48953  lincresunit2  48954  lincresunit3lem2  48956  lincresunit3  48957