Theorem resexg 6026

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-in 3911  df-ss 3921  df-res 5673

This theorem is referenced by:  resexd  6027  resex  6028  fvtresfn  6992  offres  7979  ressuppss  8178  ressuppssdif  8180  ecelqsw  8765  uniqsw  8771  eceldmqs  8784  resixp  8930  f1imaen3g  9012  dif1enlem  9143  sbthfilem  9181  fsuppres  9352  climres  15625  setsvalg  17225  setsid  17266  symgfixels  19503  qtopres  23834  vtxdginducedm1  29859  redwlk  29986  hhssva  31575  hhsssm  31576  hhshsslem1  31585  resf1o  33041  eulerpartlemmf  34731  exidres  38473  exidresid  38474  xrnresex  39024  unidmqs  39334  disjqmap2  39421  lmhmlnmsplit  43762  climresdm  46512  setsv  48072