Theorem resexg 6056

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-res 5712

This theorem is referenced by:  resexd  6057  resex  6058  fvtresfn  7031  offres  8024  ressuppss  8224  ressuppssdif  8226  resixp  8991  f1imaen3g  9076  dif1enlem  9222  dif1enlemOLD  9223  sbthfilem  9264  fsuppres  9462  climres  15621  setsvalg  17213  setsid  17255  symgfixels  19476  qtopres  23727  vtxdginducedm1  29579  redwlk  29708  hhssva  31289  hhsssm  31290  hhshsslem1  31299  resf1o  32744  eulerpartlemmf  34340  exidres  37838  exidresid  37839  xrnresex  38362  unidmqs  38610  lmhmlnmsplit  43044  climresdm  45771  setsv  47252