Theorem resexg 6020

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3945   ↾ cres 5672

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 5293

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-in 3952  df-ss 3962  df-res 5682

This theorem is referenced by:  resexd  6021  resex  6022  fvtresfn  6987  offres  7954  ressuppss  8152  ressuppssdif  8154  resixp  8912  dif1enlem  9141  dif1enlemOLD  9142  sbthfilem  9186  fsuppres  9373  climres  15503  setsvalg  17083  setsid  17125  symgfixels  19268  qtopres  23133  vtxdginducedm1  28729  redwlk  28858  hhssva  30437  hhsssm  30438  hhshsslem1  30447  resf1o  31890  eulerpartlemmf  33269  exidres  36615  exidresid  36616  xrnresex  37145  unidmqs  37393  lmhmlnmsplit  41664  climresdm  44403  setsv  45882