Theorem resexg 5985

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3884   ↾ cres 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3891  df-ss 3901  df-res 5632

This theorem is referenced by:  resexd  5986  resex  5987  fvtresfn  6941  offres  7927  ressuppss  8125  ressuppssdif  8127  ecelqsw  8709  uniqsw  8715  eceldmqs  8728  resixp  8875  f1imaen3g  8957  dif1enlem  9088  sbthfilem  9126  fsuppres  9300  climres  15532  setsvalg  17131  setsid  17172  symgfixels  19403  qtopres  23684  vtxdginducedm1  29632  redwlk  29759  hhssva  31348  hhsssm  31349  hhshsslem1  31358  resf1o  32824  eulerpartlemmf  34569  exidres  38258  exidresid  38259  xrnresex  38809  unidmqs  39119  disjqmap2  39206  lmhmlnmsplit  43545  climresdm  46305  setsv  47865