Theorem resexg 5975

Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
resexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Proof of Theorem resexg

Step	Hyp	Ref	Expression
1		resss 5949	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
2		ssexg 5259	. 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897   ↾ cres 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-res 5626

This theorem is referenced by:  resexd  5976  resex  5977  fvtresfn  6931  offres  7915  ressuppss  8113  ressuppssdif  8115  ecelqsw  8693  uniqsw  8699  eceldmqs  8711  resixp  8857  f1imaen3g  8938  dif1enlem  9069  sbthfilem  9107  fsuppres  9277  climres  15482  setsvalg  17077  setsid  17118  symgfixels  19346  qtopres  23613  vtxdginducedm1  29522  redwlk  29649  hhssva  31237  hhsssm  31238  hhshsslem1  31247  resf1o  32713  eulerpartlemmf  34388  exidres  37917  exidresid  37918  xrnresex  38452  unidmqs  38751  lmhmlnmsplit  43179  climresdm  45947  setsv  47477