Theorem resexg 5934

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3430   ⊆ wss 3891   ↾ cres 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-in 3898  df-ss 3908  df-res 5600

This theorem is referenced by:  resexd  5935  resex  5936  fvtresfn  6871  offres  7812  ressuppss  7983  ressuppssdif  7985  resixp  8695  dif1enlem  8908  sbthfilem  8949  fsuppres  9114  climres  15265  setsvalg  16848  setsid  16890  symgfixels  19023  qtopres  22830  vtxdginducedm1  27891  redwlk  28020  hhssva  29598  hhsssm  29599  hhshsslem1  29608  resf1o  31044  eulerpartlemmf  32321  exidres  36015  exidresid  36016  xrnresex  36511  unidmqs  36745  lmhmlnmsplit  40892  climresdm  43345  setsv  44782