Theorem resexg 5985

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900   ↾ cres 5625

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917  df-res 5635

This theorem is referenced by:  resexd  5986  resex  5987  fvtresfn  6943  offres  7927  ressuppss  8125  ressuppssdif  8127  ecelqsw  8707  uniqsw  8713  eceldmqs  8726  resixp  8873  f1imaen3g  8955  dif1enlem  9086  sbthfilem  9124  fsuppres  9298  climres  15500  setsvalg  17095  setsid  17136  symgfixels  19365  qtopres  23644  vtxdginducedm1  29598  redwlk  29725  hhssva  31313  hhsssm  31314  hhshsslem1  31323  resf1o  32788  eulerpartlemmf  34511  exidres  38048  exidresid  38049  xrnresex  38599  unidmqs  38909  disjqmap2  38996  lmhmlnmsplit  43366  climresdm  46131  setsv  47661