Theorem difexg 5327

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ∖ cdif 3945   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  difexi  5328  difexd  5329  difex2  7746  elpwun  7755  2oconcl  8502  fnoe  8509  difsnen  9052  sucdom2OLD  9081  fodomr  9127  domss2  9135  domssex2  9136  domssex  9137  limenpsi  9151  dif1enlem  9155  sucdom2  9205  brwdom2  9567  infeq5i  9630  infdifsn  9651  dfac8clem  10026  ssfin4  10304  isf34lem1  10366  compssiso  10368  fin1a2lem7  10400  fin1a2lem13  10406  fpwwe2lem12  10636  hashgt23el  14383  hashf1lem1OLD  14415  pmtrfv  19319  isirred  20232  isdrng2  20370  drngmcl  20373  drngid2  20377  isdrngd  20389  isdrngdOLD  20391  subdrgint  20418  cnmsubglem  21007  islindf4  21392  smadiadetlem1a  22164  basdif0  22455  tgdif0  22494  clsval2  22553  cmpcld  22905  ptcmplem2  23556  iunmbl  25069  tdeglem4OLD  25577  logbfval  26292  nbfusgrlevtxm2  28632  vtxdginducedm1  28797  frgrwopreglem1  29562  eigvecval  31144  elpwdifcl  31759  disjdifprg  31801  mptiffisupp  31910  padct  31939  resf1o  31950  xrge00  32182  xrge0tsmsd  32204  tocycf  32271  ist0cld  32808  locfinref  32816  ldsysgenld  33153  sigapildsys  33155  carsgclctun  33315  sitgclg  33336  ballotlemfrc  33520  ballotlem8  33530  bnj852  33927  bnj865  33929  subfacp1lem5  34170  iscvm  34245  cvmsval  34252  mdvval  34490  topdifinffinlem  36223  pibt2  36293  poimirlem15  36498  voliunnfl  36527  fdc  36608  isdrngo2  36821  lzenom  41498  diophin  41500  diophren  41541  deg1mhm  41939  stoweidlem57  44763  fourierdlem102  44914  fourierdlem114  44926  pwsal  45021  gsumge0cl  45077  caragendifcl  45220  carageniuncllem1  45227  isomenndlem  45236  hoidmv1lelem2  45298  lincdifsn  47095  lindslinindsimp1  47128  lindslinindimp2lem2  47130  lindslinindimp2lem4  47132  lindslinindsimp2lem5  47133  lindslinindsimp2  47134  lincresunit1  47148  lincresunit2  47149  lincresunit3lem2  47151  lincresunit3  47152