Theorem resexg 5362

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

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-res 5050

This theorem is referenced by:  resex  5363  fvtresfn  6193  offres  7054  ressuppss  7201  ressuppssdif  7203  resixp  7829  fsuppres  8183  climres  14154  setsvalg  15719  setsid  15742  symgfixels  17677  gsumval3lem1  18129  gsumval3lem2  18130  gsum2dlem2  18193  qtopres  21311  tsmspropd  21745  ulmss  23955  uhgrares  25837  umgrares  25853  usgrares  25898  usgrares1  25939  cusgrares  26001  redwlk  26136  hhssva  27498  hhsssm  27499  hhshsslem1  27508  resf1o  28893  eulerpartlemmf  29764  exidres  32847  exidresid  32848  lmhmlnmsplit  36675  pwssplit4  36677  red1wlk  40881