Theorem resexg 6019

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-in 3938  df-ss 3948  df-res 5671

This theorem is referenced by:  resexd  6020  resex  6021  fvtresfn  6993  offres  7987  ressuppss  8187  ressuppssdif  8189  resixp  8952  f1imaen3g  9035  dif1enlem  9175  dif1enlemOLD  9176  sbthfilem  9217  fsuppres  9410  climres  15596  setsvalg  17190  setsid  17231  symgfixels  19420  qtopres  23641  vtxdginducedm1  29528  redwlk  29657  hhssva  31243  hhsssm  31244  hhshsslem1  31253  resf1o  32712  eulerpartlemmf  34412  exidres  37907  exidresid  37908  xrnresex  38429  unidmqs  38677  lmhmlnmsplit  43086  climresdm  45859  setsv  47372