Theorem resexg 6014

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3898   ↾ cres 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915  df-res 5659

This theorem is used by:  resexd  6015  resex  6016  fvtresfn  6984  offres  7978  ressuppss  8178  ressuppssdif  8180  ecelqsw  8767  uniqsw  8773  eceldmqs  8786  resixp  8939  f1imaen3g  9021  dif1enlem  9153  sbthfilem  9191  fsuppres  9363  climres  15709  setsvalg  17305  setsid  17346  symgfixels  19609  qtopres  23978  vtxdginducedm1  30057  redwlk  30184  hhssva  31792  hhsssm  31793  hhshsslem1  31802  resf1o  33255  eulerpartlemmf  34941  exidres  38732  exidresid  38733  xrnresex  39281  unidmqs  39591  disjqmap2  39678  lmhmlnmsplit  44032  climresdm  46782  setsv  48382