Theorem resexg 6047

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-res 5701

This theorem is referenced by:  resexd  6048  resex  6049  fvtresfn  7018  offres  8007  ressuppss  8207  ressuppssdif  8209  resixp  8972  f1imaen3g  9055  dif1enlem  9195  dif1enlemOLD  9196  sbthfilem  9236  fsuppres  9431  climres  15608  setsvalg  17200  setsid  17242  symgfixels  19467  qtopres  23722  vtxdginducedm1  29576  redwlk  29705  hhssva  31286  hhsssm  31287  hhshsslem1  31296  resf1o  32748  eulerpartlemmf  34357  exidres  37865  exidresid  37866  xrnresex  38388  unidmqs  38636  lmhmlnmsplit  43076  climresdm  45806  setsv  47303