Theorem resexg 5987

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-res 5643

This theorem is referenced by:  resexd  5988  resex  5989  fvtresfn  6952  offres  7941  ressuppss  8139  ressuppssdif  8141  ecelqsw  8719  uniqsw  8725  eceldmqs  8737  resixp  8883  f1imaen3g  8964  dif1enlem  9097  dif1enlemOLD  9098  sbthfilem  9139  fsuppres  9320  climres  15518  setsvalg  17113  setsid  17154  symgfixels  19349  qtopres  23619  vtxdginducedm1  29525  redwlk  29652  hhssva  31237  hhsssm  31238  hhshsslem1  31247  resf1o  32704  eulerpartlemmf  34360  exidres  37866  exidresid  37867  xrnresex  38386  unidmqs  38640  lmhmlnmsplit  43070  climresdm  45842  setsv  47373