Theorem resexg 5979

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   ⊆ wss 3883   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-res 5630

This theorem is referenced by:  resexd  5980  resex  5981  fvtresfn  6938  offres  7925  ressuppss  8123  ressuppssdif  8125  ecelqsw  8705  uniqsw  8711  eceldmqs  8724  resixp  8871  f1imaen3g  8953  dif1enlem  9084  sbthfilem  9122  fsuppres  9296  climres  15528  setsvalg  17127  setsid  17168  symgfixels  19400  qtopres  23681  vtxdginducedm1  29630  redwlk  29757  hhssva  31346  hhsssm  31347  hhshsslem1  31356  resf1o  32822  eulerpartlemmf  34559  exidres  38245  exidresid  38246  xrnresex  38796  unidmqs  39106  disjqmap2  39193  lmhmlnmsplit  43532  climresdm  46293  setsv  47853