Theorem resexg 6015

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906   ↾ cres 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-res 5661

This theorem is referenced by:  resexd  6016  resex  6017  fvtresfn  6980  offres  7966  ressuppss  8165  ressuppssdif  8167  ecelqsw  8752  uniqsw  8758  eceldmqs  8771  resixp  8917  f1imaen3g  8999  dif1enlem  9130  sbthfilem  9168  fsuppres  9341  climres  15604  setsvalg  17204  setsid  17245  symgfixels  19476  qtopres  23760  vtxdginducedm1  29746  redwlk  29873  hhssva  31462  hhsssm  31463  hhshsslem1  31472  resf1o  32934  eulerpartlemmf  34674  exidres  38382  exidresid  38383  xrnresex  38933  unidmqs  39243  disjqmap2  39330  lmhmlnmsplit  43669  climresdm  46429  setsv  47989